Я определил свои пропозициональные формулы следующим образом: Inductive propForm : Set := | top : propForm | bot : propForm | var : propVar -> propForm | orp : propForm -> propForm -> propForm | andp : propForm -> propForm ->...

При доказывании в Coq приятно иметь возможность доказывать по одному кусочку за раз, а Coq помогает отслеживать обязательства. Theorem ModusPonens: forall (A B : Prop), ((A -> B) /\ A) -> B. Proof. intros A B [H1 H2]. apply H1. На...