update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_1 / subst0 / props.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_1/subst0/props.ma b/matita/matita/contribs/lambdadelta/basic_1/subst0/props.ma
index 5da05fa2ad5e5a13e50f88a54e536139e3271600..762f857620b7b76de4419d69abaf4ae08330e9cf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/subst0/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/subst0/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/subst0/fwd.ma".
+include "basic_1/subst0/fwd.ma".
 
-theorem subst0_refl:
+lemma subst0_refl:
  \forall (u: T).(\forall (t: T).(\forall (d: nat).((subst0 d u t t) \to 
 (\forall (P: Prop).P))))
 \def
@@ -43,42 +43,37 @@ T).(subst0 (s k d) u t1 t2)))) P (\lambda (H2: (ex2 T (\lambda (u2: T).(eq T
 u2)))).(ex2_ind T (\lambda (u2: T).(eq T (THead k t0 t1) (THead k u2 t1))) 
 (\lambda (u2: T).(subst0 d u t0 u2)) P (\lambda (x: T).(\lambda (H3: (eq T 
 (THead k t0 t1) (THead k x t1))).(\lambda (H4: (subst0 d u t0 x)).(let H5 
-\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) 
-with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead _ t2 _) 
-\Rightarrow t2])) (THead k t0 t1) (THead k x t1) H3) in (let H6 \def 
-(eq_ind_r T x (\lambda (t2: T).(subst0 d u t0 t2)) H4 t0 H5) in (H d H6 
-P)))))) H2)) (\lambda (H2: (ex2 T (\lambda (t2: T).(eq T (THead k t0 t1) 
-(THead k t0 t2))) (\lambda (t2: T).(subst0 (s k d) u t1 t2)))).(ex2_ind T 
-(\lambda (t2: T).(eq T (THead k t0 t1) (THead k t0 t2))) (\lambda (t2: 
-T).(subst0 (s k d) u t1 t2)) P (\lambda (x: T).(\lambda (H3: (eq T (THead k 
-t0 t1) (THead k t0 x))).(\lambda (H4: (subst0 (s k d) u t1 x)).(let H5 \def 
-(f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with 
-[(TSort _) \Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ _ t2) 
-\Rightarrow t2])) (THead k t0 t1) (THead k t0 x) H3) in (let H6 \def 
-(eq_ind_r T x (\lambda (t2: T).(subst0 (s k d) u t1 t2)) H4 t1 H5) in (H0 (s 
-k d) H6 P)))))) H2)) (\lambda (H2: (ex3_2 T T (\lambda (u2: T).(\lambda (t2: 
-T).(eq T (THead k t0 t1) (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: 
-T).(subst0 d u t0 u2))) (\lambda (_: T).(\lambda (t2: T).(subst0 (s k d) u t1 
-t2))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead k t0 
+\def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 | 
+(TLRef _) \Rightarrow t0 | (THead _ t2 _) \Rightarrow t2])) (THead k t0 t1) 
+(THead k x t1) H3) in (let H6 \def (eq_ind_r T x (\lambda (t2: T).(subst0 d u 
+t0 t2)) H4 t0 H5) in (H d H6 P)))))) H2)) (\lambda (H2: (ex2 T (\lambda (t2: 
+T).(eq T (THead k t0 t1) (THead k t0 t2))) (\lambda (t2: T).(subst0 (s k d) u 
+t1 t2)))).(ex2_ind T (\lambda (t2: T).(eq T (THead k t0 t1) (THead k t0 t2))) 
+(\lambda (t2: T).(subst0 (s k d) u t1 t2)) P (\lambda (x: T).(\lambda (H3: 
+(eq T (THead k t0 t1) (THead k t0 x))).(\lambda (H4: (subst0 (s k d) u t1 
+x)).(let H5 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) 
+\Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ _ t2) \Rightarrow t2])) 
+(THead k t0 t1) (THead k t0 x) H3) in (let H6 \def (eq_ind_r T x (\lambda 
+(t2: T).(subst0 (s k d) u t1 t2)) H4 t1 H5) in (H0 (s k d) H6 P)))))) H2)) 
+(\lambda (H2: (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead k t0 
 t1) (THead k u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(subst0 d u t0 u2))) 
-(\lambda (_: T).(\lambda (t2: T).(subst0 (s k d) u t1 t2))) P (\lambda (x0: 
-T).(\lambda (x1: T).(\lambda (H3: (eq T (THead k t0 t1) (THead k x0 
-x1))).(\lambda (H4: (subst0 d u t0 x0)).(\lambda (H5: (subst0 (s k d) u t1 
-x1)).(let H6 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda 
-(_: T).T) with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | (THead 
-_ t2 _) \Rightarrow t2])) (THead k t0 t1) (THead k x0 x1) H3) in ((let H7 
-\def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) 
-with [(TSort _) \Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ _ t2) 
+(\lambda (_: T).(\lambda (t2: T).(subst0 (s k d) u t1 t2))))).(ex3_2_ind T T 
+(\lambda (u2: T).(\lambda (t2: T).(eq T (THead k t0 t1) (THead k u2 t2)))) 
+(\lambda (u2: T).(\lambda (_: T).(subst0 d u t0 u2))) (\lambda (_: 
+T).(\lambda (t2: T).(subst0 (s k d) u t1 t2))) P (\lambda (x0: T).(\lambda 
+(x1: T).(\lambda (H3: (eq T (THead k t0 t1) (THead k x0 x1))).(\lambda (H4: 
+(subst0 d u t0 x0)).(\lambda (H5: (subst0 (s k d) u t1 x1)).(let H6 \def 
+(f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 | (TLRef 
+_) \Rightarrow t0 | (THead _ t2 _) \Rightarrow t2])) (THead k t0 t1) (THead k 
+x0 x1) H3) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e with 
+[(TSort _) \Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ _ t2) 
 \Rightarrow t2])) (THead k t0 t1) (THead k x0 x1) H3) in (\lambda (H8: (eq T 
 t0 x0)).(let H9 \def (eq_ind_r T x1 (\lambda (t2: T).(subst0 (s k d) u t1 
 t2)) H5 t1 H7) in (let H10 \def (eq_ind_r T x0 (\lambda (t2: T).(subst0 d u 
 t0 t2)) H4 t0 H8) in (H d H10 P))))) H6))))))) H2)) (subst0_gen_head k u t0 
 t1 (THead k t0 t1) d H1)))))))))) t)).
-(* COMMENTS
-Initial nodes: 1119
-END *)
 
-theorem subst0_lift_lt:
+lemma subst0_lift_lt:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0 
 i u t1 t2) \to (\forall (d: nat).((lt i d) \to (\forall (h: nat).(subst0 i 
 (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2)))))))))
@@ -147,11 +142,8 @@ k i0) (lift h n v) (lift h (s k d) t0) (lift h (s k d) t3))) (H5 (s k d)
 (s_lt k i0 d H4) h) (minus d (S i0)) (minus_s_s k d (S i0)))) (lift h d 
 (THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d (THead k u1 t0)) 
 (lift_head k u1 t0 h d))))))))))))))))) i u t1 t2 H))))).
-(* COMMENTS
-Initial nodes: 1805
-END *)
 
-theorem subst0_lift_ge:
+lemma subst0_lift_ge:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).(\forall 
 (h: nat).((subst0 i u t1 t2) \to (\forall (d: nat).((le d i) \to (subst0 
 (plus i h) u (lift h d t1) (lift h d t2)))))))))
@@ -208,11 +200,8 @@ h (s k d) t3)) (\lambda (t: T).(subst0 (plus i0 h) v (THead k (lift h d u1)
 h) (H1 d H4) k (lift h (s k d) t0) (lift h (s k d) t3) (H5 (s k d) (s_le k d 
 i0 H4))) (lift h d (THead k u2 t3)) (lift_head k u2 t3 h d)) (lift h d (THead 
 k u1 t0)) (lift_head k u1 t0 h d)))))))))))))))) i u t1 t2 H)))))).
-(* COMMENTS
-Initial nodes: 1449
-END *)
 
-theorem subst0_lift_ge_S:
+lemma subst0_lift_ge_S:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0 
 i u t1 t2) \to (\forall (d: nat).((le d i) \to (subst0 (S i) u (lift (S O) d 
 t1) (lift (S O) d t2))))))))
@@ -221,13 +210,10 @@ t1) (lift (S O) d t2))))))))
 (H: (subst0 i u t1 t2)).(\lambda (d: nat).(\lambda (H0: (le d i)).(eq_ind nat 
 (plus i (S O)) (\lambda (n: nat).(subst0 n u (lift (S O) d t1) (lift (S O) d 
 t2))) (subst0_lift_ge t1 t2 u i (S O) H d H0) (S i) (eq_ind_r nat (plus (S O) 
-i) (\lambda (n: nat).(eq nat n (S i))) (refl_equal nat (S i)) (plus i (S O)) 
-(plus_sym i (S O)))))))))).
-(* COMMENTS
-Initial nodes: 137
-END *)
+i) (\lambda (n: nat).(eq nat n (S i))) (le_antisym (plus (S O) i) (S i) (le_n 
+(S i)) (le_n (plus (S O) i))) (plus i (S O)) (plus_sym i (S O)))))))))).
 
-theorem subst0_lift_ge_s:
+lemma subst0_lift_ge_s:
  \forall (t1: T).(\forall (t2: T).(\forall (u: T).(\forall (i: nat).((subst0 
 i u t1 t2) \to (\forall (d: nat).((le d i) \to (\forall (b: B).(subst0 (s 
 (Bind b) i) u (lift (S O) d t1) (lift (S O) d t2)))))))))
@@ -235,7 +221,4 @@ i u t1 t2) \to (\forall (d: nat).((le d i) \to (\forall (b: B).(subst0 (s
  \lambda (t1: T).(\lambda (t2: T).(\lambda (u: T).(\lambda (i: nat).(\lambda 
 (H: (subst0 i u t1 t2)).(\lambda (d: nat).(\lambda (H0: (le d i)).(\lambda 
 (_: B).(subst0_lift_ge_S t1 t2 u i H d H0)))))))).
-(* COMMENTS
-Initial nodes: 43
-END *)