]> matita.cs.unibo.it Git - helm.git/commitdiff
M logic/coimplication.ma
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 18 Dec 2006 12:01:11 +0000 (12:01 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 18 Dec 2006 12:01:11 +0000 (12:01 +0000)
helm/software/matita/library/logic/coimplication.ma

index 9edb4949c532c23ee43679ae11ad2ecac123d4bf..24965d72ce063f6209259812b1b189b661a5f331 100644 (file)
@@ -39,9 +39,9 @@ theorem iff_refl: \forall A. A \liff A.
 qed.
 
 theorem iff_sym: \forall A,B. A \liff B \to B \liff A.
- intros. decompose. apply iff_intro; intros; auto.
+ intros. elim H. apply iff_intro[assumption|assumption]
 qed.
 
 theorem iff_trans: \forall A,B,C. A \liff B \to B \liff C \to A \liff C.
- intros. decompose. apply iff_intro; intros; auto.
+ intros. elim H. elim H1. apply iff_intro;intros;auto.
 qed.