X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Flegacy_1%2Fcoq%2Fprops.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Flegacy_1%2Fcoq%2Fprops.ma;h=a9223f1b14f63fea039caaf1cfbf3f9d7ec2a245;hb=24b593925bae7964bdc61e28408d389e5a74bd7a;hp=83e2b707e840a53fc175f6cc1b813a5185382897;hpb=38d63e5adf7f0eeeab575697e10c2867cc1c2a7f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma
index 83e2b707e..a9223f1b1 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma
@@ -77,8 +77,8 @@ theorem eq_ind_r:
 (\forall (y: A).((eq A y x) \to (P y))))))
 \def
  \lambda (A: Type[0]).(\lambda (x: A).(\lambda (P: ((A \to Prop))).(\lambda 
-(H: (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(match (sym_eq A y x H0) 
-with [refl_equal \Rightarrow H])))))).
+(H: (P x)).(\lambda (y: A).(\lambda (H0: (eq A y x)).(let TMP_1 \def (sym_eq 
+A y x H0) in (match TMP_1 with [refl_equal \Rightarrow H]))))))).
 
 theorem trans_eq:
  \forall (A: Type[0]).(\forall (x: A).(\forall (y: A).(\forall (z: A).((eq A