前回に引き続き、練習してます。今回はちょうど見つけたCoq-99 : Part 1の問題をやってみました。一応、答えを見ずに全部できましたが、所々詰まったりしました。ある意味、人間バックトラックです。 Lemma Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B)…