severe bug found in parallel zeta

[helm.git] / helm / software / matita / library / logic / coimplication.ma

diff --git a/helm/software/matita/library/logic/coimplication.ma b/helm/software/matita/library/logic/coimplication.ma
index 67f04b90308b28e8632c9ddf266d7e86e99ff246..44f8d5b8eb5f5f36f4affe1aefe4bb334ae6882b 100644 (file)
--- 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.