X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Ftechnicalities%2Fsetoids.ma;h=c440795ffc2a099ee041fbe8039bc5f20bf478f3;hb=894c3e4038c93b484896e81132eae55046e47605;hp=d730d06de6a60386a43b28c2132dbcdcb0b2568a;hpb=c48de1fba2742df0d3ab42d69e758ae2859316d0;p=helm.git

diff --git a/helm/software/matita/library/technicalities/setoids.ma b/helm/software/matita/library/technicalities/setoids.ma
index d730d06de..c440795ff 100644
--- a/helm/software/matita/library/technicalities/setoids.ma
+++ b/helm/software/matita/library/technicalities/setoids.ma
@@ -245,7 +245,8 @@ definition equality_morphism_of_symmetric_reflexive_transitive_relation:
     split;
     intro;
     unfold transitive in H;
-    auto
+    unfold symmetric in sym;
+    auto.
   ]
 qed.