X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Flogic%2Fequality.ma;h=b87dc6c95656dcf5de3c3ceb00e9ed105067c6b8;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=70ade5589c46f0eb073a7d991d41dd7a19ab2eaa;hpb=69dc6031c9e0574fa7a74ced74deeb7f9ec5695b;p=helm.git

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 70ade5589..b87dc6c95 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -32,8 +32,7 @@ theorem eq_ind':
   P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p.
  intros.
  exact
-  ([\lambda y:A. \lambda p:eq A x y.P y p]
-   match p with
+  (match p return \lambda y. \lambda p.P y p with
     [refl_eq \Rightarrow H]).
 qed.
  
@@ -42,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