Αποστολή με SMS: Απόδειξη ορθότητας του μετασχηματισμού διακλαδιζόμενων διαστάσεων στο coq /