「Aならば、AならばBならばB」の証明はCoq*1だと以下のように書けます。 Goal forall (A B : Prop), A -> (A -> B) -> B. Proof. intros A B. intro. intro. apply H0. apply H. Qed.なんでこれが証明になっているんでしょうか。Coqのモデルは自然演繹*2だそ…