X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Flogic%2Fequality.ma;h=b87dc6c95656dcf5de3c3ceb00e9ed105067c6b8;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=40157d849f9baf53e9f871f07ef5432adba152c9;hpb=8530992b72238902faae5e8bff74550fd8d7264a;p=helm.git

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 40157d849..b87dc6c95 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -41,14 +41,14 @@ simplify.intros.apply refl_eq.
 qed.
     
 theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
-simplify.intros.elim H. apply refl_eq.
+unfold symmetric.intros.elim H. apply refl_eq.
 qed.
 
 theorem sym_eq : \forall A:Type.\forall x,y:A. x=y  \to y=x
 \def symmetric_eq.
 
 theorem transitive_eq : \forall A:Type. transitive A (eq A).
-simplify.intros.elim H1.assumption.
+unfold transitive.intros.elim H1.assumption.
 qed.
 
 theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z