some improvements in the anticipator

[helm.git] / matita / matita / contribs / lambdadelta / legacy_1 / coq / props.ma

diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/props.ma
index 83e2b707e840a53fc175f6cc1b813a5185382897..a9223f1b14f63fea039caaf1cfbf3f9d7ec2a245 100644 (file)
--- 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