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: 0.4.95@7852~723
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eacb4cecf5753579268fbadb2ed64d1a987b7629;p=helm.git

M    logic/coimplication.ma
---

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