X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Falgebra%2FCoRN%2FSetoidFun.ma;h=67f8ac1d6a5763dfab65e15b17128ed1d3f66b85;hb=0b69be40774bf7f75c8ed8a75c02998437ebbdbb;hp=d78aac70e07e6abc655bc9aa9e4834e1a6479400;hpb=8e24e39aed25a2c31fb7073308ee3f0b80c206e6;p=helm.git

diff --git a/matita/library/algebra/CoRN/SetoidFun.ma b/matita/library/algebra/CoRN/SetoidFun.ma
index d78aac70e..67f8ac1d6 100644
--- a/matita/library/algebra/CoRN/SetoidFun.ma
+++ b/matita/library/algebra/CoRN/SetoidFun.ma
@@ -1247,7 +1247,8 @@ a = b \to b \neq c \to a \neq c.
 intros.
 generalize in match (ap_cotransitive_unfolded ? ? ? H1 a).
 intro.elim H2.apply False_ind.apply (eq_imp_not_ap ? ? ? H).
-autobatch.assumption.
+apply ap_symmetric_unfolded. assumption.
+assumption.
 qed.
 
 lemma Dir_bij : \forall A, B:CSetoid.