2010-09-26 を見て同じ命題を Agda2 で証明してみた。 Functional Programming Memo: [Coq] Coq-99 : Part 1 agda-mode が証明するのを手伝ってくれるのでお気楽です。 module Practice1 where data True : Prop where tt : True data False : Prop where data _∧_ (P Q : Prop) : Prop where ∧-intro : P → Q → P ∧ Q ∧-eliml : ∀ {P Q} → P ∧ Q → P ∧-eliml (∧-intro y y') = y ∧-elimr : ∀ {P Q} -> P ∧ Q -> Q ∧-elimr (∧-intro y y') = y' data _∨_ (P Q : Prop) : P