update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / s / fwd.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma b/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma
index c9ab5dbfcf8be0d317f611038dbbea19fd7bf95b..deac2dbd3e4604f4cc439391ae3655f2321aee13 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/s/fwd.ma
@@ -16,36 +16,33 @@
 
 include "basic_1/s/defs.ma".
 
-theorem s_inj:
+lemma 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:
+lemma 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:
+lemma 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).