Logical Foundationsを進めがてら、基礎固め的に簡単な命題論理の命題を証明してみたいと思ってググったらこんなスレに遭遇した： coq.discourse.group このうちの最初の問題が簡単ながらもいくつか面白い点があったのでメモ。 証明する命題： Lemma a1 : fo…