something was really too slow...

[helm.git] / helm / software / matita / library / algebra / CoRN / SetoidFun.ma

diff --git a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma b/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
index d78aac70e07e6abc655bc9aa9e4834e1a6479400..67f8ac1d6a5763dfab65e15b17128ed1d3f66b85 100644 (file)
--- a/helm/software/matita/library/algebra/CoRN/SetoidFun.ma
+++ b/helm/software/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.