X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Flegacy_1%2Fcoq%2Ffwd.ma;h=8738e723477753937d43b49254e1449b438b7f0d;hb=639e798161afea770f41d78673c0fe3be4125beb;hp=5e19eab759ecf1f7baf246d7b39b71bc2a390e86;hpb=15455aa487e001c643b4f46daf82612b8409f1ae;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
index 5e19eab75..8738e7234 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
@@ -83,13 +83,12 @@ x P))).
 
 let rec le_ind (n: nat) (P: (nat \to Prop)) (f: P n) (f0: (\forall (m: 
 nat).((le n m) \to ((P m) \to (P (S m)))))) (n0: nat) (l: le n n0) on l: P n0 
-\def match l with [le_n \Rightarrow f | (le_S m l0) \Rightarrow (let TMP_1 
-\def ((le_ind n P f f0) m l0) in (f0 m l0 TMP_1))].
+\def match l with [le_n \Rightarrow f | (le_S m l0) \Rightarrow (f0 m l0 
+((le_ind n P f f0) m l0))].
 
 let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to Prop)) (f: 
 (\forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to (((\forall 
 (y: A).((R y x) \to (P y)))) \to (P x))))) (a: A) (a0: Acc A R a) on a0: P a 
-\def match a0 with [(Acc_intro x a1) \Rightarrow (let TMP_2 \def (\lambda (y: 
-A).(\lambda (r: (R y x)).(let TMP_1 \def (a1 y r) in ((Acc_ind A R P f) y 
-TMP_1)))) in (f x a1 TMP_2))].
+\def match a0 with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda (y: 
+A).(\lambda (r: (R y x)).((Acc_ind A R P f) y (a1 y r)))))].