X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Flogic%2Fcoimplication.ma;h=24965d72ce063f6209259812b1b189b661a5f331;hb=909cdbb5ddf942e75558149c9f11819c6c84bc3a;hp=9edb4949c532c23ee43679ae11ad2ecac123d4bf;hpb=62596f4e0a109e43c9df5da20571827c8b905ce4;p=helm.git

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.