X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fs%2Ffwd.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fs%2Ffwd.ma;h=48a34e79b3a34c5469f80330780bbe21c5695eae;hb=639e798161afea770f41d78673c0fe3be4125beb;hp=c9ab5dbfcf8be0d317f611038dbbea19fd7bf95b;hpb=15455aa487e001c643b4f46daf82612b8409f1ae;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma
index c9ab5dbfc..48a34e79b 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma
@@ -20,32 +20,29 @@ theorem s_inj:
  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((eq nat (s k i) (s k j)) 
 \to (eq nat i j))))
 \def
- \lambda (k: K).(let TMP_1 \def (\lambda (k0: K).(\forall (i: nat).(\forall 
-(j: nat).((eq nat (s k0 i) (s k0 j)) \to (eq nat i j))))) in (let TMP_2 \def 
-(\lambda (b: B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (eq nat (s 
-(Bind b) i) (s (Bind b) j))).(eq_add_S i j H))))) in (let TMP_3 \def (\lambda 
-(f: F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (eq nat (s (Flat f) 
-i) (s (Flat f) j))).H)))) in (K_ind TMP_1 TMP_2 TMP_3 k)))).
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: 
+nat).((eq nat (s k0 i) (s k0 j)) \to (eq nat i j))))) (\lambda (b: 
+B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (eq nat (s (Bind b) i) (s 
+(Bind b) j))).(eq_add_S i j H))))) (\lambda (f: F).(\lambda (i: nat).(\lambda 
+(j: nat).(\lambda (H: (eq nat (s (Flat f) i) (s (Flat f) j))).H)))) k).
 
 theorem s_le_gen:
  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((le (s k i) (s k j)) \to 
 (le i j))))
 \def
- \lambda (k: K).(let TMP_1 \def (\lambda (k0: K).(\forall (i: nat).(\forall 
-(j: nat).((le (s k0 i) (s k0 j)) \to (le i j))))) in (let TMP_2 \def (\lambda 
-(b: B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (le (s (Bind b) i) (s 
-(Bind b) j))).(le_S_n i j H))))) in (let TMP_3 \def (\lambda (f: F).(\lambda 
-(i: nat).(\lambda (j: nat).(\lambda (H: (le (s (Flat f) i) (s (Flat f) 
-j))).H)))) in (K_ind TMP_1 TMP_2 TMP_3 k)))).
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: 
+nat).((le (s k0 i) (s k0 j)) \to (le i j))))) (\lambda (b: B).(\lambda (i: 
+nat).(\lambda (j: nat).(\lambda (H: (le (s (Bind b) i) (s (Bind b) 
+j))).(le_S_n i j H))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (j: 
+nat).(\lambda (H: (le (s (Flat f) i) (s (Flat f) j))).H)))) k).
 
 theorem s_lt_gen:
  \forall (k: K).(\forall (i: nat).(\forall (j: nat).((lt (s k i) (s k j)) \to 
 (lt i j))))
 \def
- \lambda (k: K).(let TMP_1 \def (\lambda (k0: K).(\forall (i: nat).(\forall 
-(j: nat).((lt (s k0 i) (s k0 j)) \to (lt i j))))) in (let TMP_3 \def (\lambda 
-(b: B).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (lt (s (Bind b) i) (s 
-(Bind b) j))).(let TMP_2 \def (S i) in (le_S_n TMP_2 j H)))))) in (let TMP_4 
-\def (\lambda (f: F).(\lambda (i: nat).(\lambda (j: nat).(\lambda (H: (lt (s 
-(Flat f) i) (s (Flat f) j))).H)))) in (K_ind TMP_1 TMP_3 TMP_4 k)))).
+ \lambda (k: K).(K_ind (\lambda (k0: K).(\forall (i: nat).(\forall (j: 
+nat).((lt (s k0 i) (s k0 j)) \to (lt i j))))) (\lambda (b: B).(\lambda (i: 
+nat).(\lambda (j: nat).(\lambda (H: (lt (s (Bind b) i) (s (Bind b) 
+j))).(le_S_n (S i) j H))))) (\lambda (f: F).(\lambda (i: nat).(\lambda (j: 
+nat).(\lambda (H: (lt (s (Flat f) i) (s (Flat f) j))).H)))) k).