-lemma dmg : ¬(A ∨ B) ⇒ ¬A ∧ ¬B.
-
- apply (prove (¬(A ∨ B) ⇒ ¬A ∧ ¬B));
- apply (⇒_i [H] (¬A ∧ ¬B));
-
- apply (¬_e (¬A) A);
-
-
-
-
-(*
-lemma ex2: ΠN:Type.ΠR:N→N→CProp.
-
- (∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y.
-
- intros (N R);apply (prove ((∀a:N.∀b:N.R a b ⇒ R b a) ⇒ ∀z:N.(∃x.R x z) ⇒ ∃y. R z y));
-
- apply (⇒_i [H] (∀z:N.(∃x:N.R x z)⇒∃y:N.R z y));
- apply (∀_i [z] ((∃x:N.R x z)⇒∃y:N.R z y));
- apply (⇒_i [H2] (∃y:N.R z y));
- apply (∃_e (∃x:N.R x z) [n] [H3] (∃y:N.R z y));
- [ apply [H2]
- | apply (∃_i n (R z n));
- apply (⇒_e (R n z ⇒ R z n) (R n z));
- [ apply (∀_e (∀b:N.R n b ⇒ R b n) z);
- apply (∀_e (∀a:N.∀b:N.R a b ⇒ R b a) n);
- apply [H]
- | apply [H3]
- ]
- ]
-qed.
-*)
\ No newline at end of file