From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 18 Dec 2006 12:01:11 +0000 (+0000)
Subject: M    logic/coimplication.ma
X-Git-Tag: make_still_working~6582
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c63590f609ffda64f0af782bccb127e1701c34d7;p=helm.git

M    logic/coimplication.ma
---

diff --git a/helm/software/matita/library/logic/coimplication.ma b/helm/software/matita/library/logic/coimplication.ma
index 9edb4949c..24965d72c 100644
--- a/helm/software/matita/library/logic/coimplication.ma
+++ b/helm/software/matita/library/logic/coimplication.ma
@@ -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.