From eacb4cecf5753579268fbadb2ed64d1a987b7629 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 18 Dec 2006 12:01:11 +0000 Subject: [PATCH] M logic/coimplication.ma --- matita/library/logic/coimplication.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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. -- 2.39.2