X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Flogic%2Fcoimplication.ma;h=44f8d5b8eb5f5f36f4affe1aefe4bb334ae6882b;hb=6d49221c1fefe6a2c5bddb3db24d3698414a700f;hp=67f04b90308b28e8632c9ddf266d7e86e99ff246;hpb=42c44d828983e4ea2d115eba20a8020b62108384;p=helm.git

diff --git a/helm/software/matita/library/logic/coimplication.ma b/helm/software/matita/library/logic/coimplication.ma
index 67f04b903..44f8d5b8e 100644
--- a/helm/software/matita/library/logic/coimplication.ma
+++ b/helm/software/matita/library/logic/coimplication.ma
@@ -32,5 +32,5 @@ theorem iff_sym: \forall A,B. A \liff B \to B \liff A.
 qed.
 
 theorem iff_trans: \forall A,B,C. A \liff B \to B \liff C \to A \liff C.
- intros. elim H. elim H1. apply iff_intro;intros;autobatch.
+ intros. elim H. elim H1. apply iff_intro;intros;autobatch depth=3.
 qed.