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

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 7e67c056c..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. \lambda p.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