X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Flegacy_1%2Fcoq%2Fdefs.ma;h=b059133d94c02c0fdc9f82938b05c76ccca1946d;hb=9c954a9a843ebb1bf189536df4e14f77132ed1cf;hp=75e58b0364f93ac5077e8fb475a8ce0d70517b29;hpb=e51d01099c08e9945ea093da6fcac353db7ca23c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
index 75e58b036..b059133d9 100644
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/defs.ma
@@ -55,7 +55,7 @@ inductive le (n: nat): nat \to Prop \def
 definition lt:
  nat \to (nat \to Prop)
 \def
- \lambda (n: nat).(\lambda (m: nat).(le (S n) m)).
+ \lambda (n: nat).(\lambda (m: nat).(let TMP_1 \def (S n) in (le TMP_1 m))).
 
 definition IsSucc:
  nat \to Prop
@@ -69,7 +69,8 @@ definition pred:
  \lambda (n: nat).(match n with [O \Rightarrow O | (S u) \Rightarrow u]).
 
 let rec plus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with 
-[O \Rightarrow m | (S p) \Rightarrow (S (plus p m))]).
+[O \Rightarrow m | (S p) \Rightarrow (let TMP_2 \def (plus p m) in (S 
+TMP_2))]).
 
 let rec minus (n: nat) on n: nat \to nat \def \lambda (m: nat).(match n with 
 [O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k) | (S 
@@ -89,5 +90,6 @@ definition ltof:
  \forall (A: Type[0]).(((A \to nat)) \to (A \to (A \to Prop)))
 \def
  \lambda (A: Type[0]).(\lambda (f: ((A \to nat))).(\lambda (a: A).(\lambda 
-(b: A).(lt (f a) (f b))))).
+(b: A).(let TMP_4 \def (f a) in (let TMP_3 \def (f b) in (lt TMP_4 
+TMP_3)))))).