]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 27 Sep 2006 16:19:17 +0000 (16:19 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 27 Sep 2006 16:19:17 +0000 (16:19 +0000)
helm/software/matita/library/technicalities/setoids.ma

index d730d06de6a60386a43b28c2132dbcdcb0b2568a..c440795ffc2a099ee041fbe8039bc5f20bf478f3 100644 (file)
@@ -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.