Procedural : tentative update to the new letin cic construction

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / LambdaDelta-1 / subst0 / subst0.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma
index b234990eef9ce0f6df1079df2ff7527cb5ef3818..43747913fc3f775e726abc76eb3c53f3e55053c8 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma
@@ -293,7 +293,7 @@ T).(\forall (u2: T).(\forall (i2: nat).((subst0 i2 u2 t2 t4) \to ((not (eq
 nat n i2)) \to (ex2 T (\lambda (t5: T).(subst0 i2 u2 t3 t5)) (\lambda (t5: 
 T).(subst0 n t t4 t5)))))))))))) (\lambda (v: T).(\lambda (i: nat).(\lambda 
 (t2: T).(\lambda (u2: T).(\lambda (i2: nat).(\lambda (H0: (subst0 i2 u2 
-(TLRef i) t2)).(\lambda (H1: (not (eq nat i i2))).(and_ind (eq nat i i2) (eq 
+(TLRef i) t2)).(\lambda (H1: (not (eq nat i i2))).(land_ind (eq nat i i2) (eq 
 T t2 (lift (S i) O u2)) (ex2 T (\lambda (t: T).(subst0 i2 u2 (lift (S i) O v) 
 t)) (\lambda (t: T).(subst0 i v t2 t))) (\lambda (H2: (eq nat i i2)).(\lambda 
 (H3: (eq T t2 (lift (S i) O u2))).(let H4 \def (eq_ind nat i (\lambda (n: 
@@ -394,10 +394,14 @@ T).(subst0 i2 u2 (THead k u t2) t5)) (\lambda (t5: T).(subst0 i v t t5))))
 (subst0 (s k i2) u2 t2 x0)).(\lambda (H8: (subst0 (s k i) v x x0)).(ex_intro2 
 T (\lambda (t: T).(subst0 i2 u2 (THead k u t2) t)) (\lambda (t: T).(subst0 i 
 v (THead k u x) t)) (THead k u x0) (subst0_snd k u2 x0 t2 i2 H7 u) 
-(subst0_snd k v x0 x i H8 u))))) (H1 x u2 (s k i2) H6 (\lambda (H7: (eq nat 
-(s k i) (s k i2))).(H3 (s_inj k i i2 H7))))) t4 H5)))) H4)) (\lambda (H4: 
-(ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3 t5)))) 
-(\lambda (u3: T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_: 
+(subst0_snd k v x0 x i H8 u))))) (H1 x u2 (s k i2) H6 (ex2_ind T (\lambda (t: 
+T).(subst0 (s k i2) u2 t2 t)) (\lambda (t: T).(subst0 (s k i) v x t)) ((eq 
+nat (s k i) (s k i2)) \to False) (\lambda (x0: T).(\lambda (_: (subst0 (s k 
+i2) u2 t2 x0)).(\lambda (_: (subst0 (s k i) v x x0)).(\lambda (H9: (eq nat (s 
+k i) (s k i2))).(H3 (s_inj k i i2 H9)))))) (H1 x u2 (s k i2) H6 (\lambda (H7: 
+(eq nat (s k i) (s k i2))).(H3 (s_inj k i i2 H7))))))) t4 H5)))) H4)) 
+(\lambda (H4: (ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq T t4 (THead k 
+u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_: 
 T).(\lambda (t5: T).(subst0 (s k i2) u2 t3 t5))))).(ex3_2_ind T T (\lambda 
 (u3: T).(\lambda (t5: T).(eq T t4 (THead k u3 t5)))) (\lambda (u3: 
 T).(\lambda (_: T).(subst0 i2 u2 u u3))) (\lambda (_: T).(\lambda (t5: 
@@ -413,20 +417,24 @@ x1) t))) (\lambda (x: T).(\lambda (H8: (subst0 (s k i2) u2 t2 x)).(\lambda
 (H9: (subst0 (s k i) v x1 x)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u2 
 (THead k u t2) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t)) (THead k 
 x0 x) (subst0_both u2 u x0 i2 H6 k t2 x H8) (subst0_snd k v x x1 i H9 x0))))) 
-(H1 x1 u2 (s k i2) H7 (\lambda (H8: (eq nat (s k i) (s k i2))).(H3 (s_inj k i 
-i2 H8))))) t4 H5)))))) H4)) (subst0_gen_head k u2 u t3 t4 i2 
-H2))))))))))))))) (\lambda (v: T).(\lambda (u0: T).(\lambda (u2: T).(\lambda 
-(i: nat).(\lambda (H0: (subst0 i v u0 u2)).(\lambda (H1: ((\forall (t2: 
-T).(\forall (u3: T).(\forall (i2: nat).((subst0 i2 u3 u0 t2) \to ((not (eq 
-nat i i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: 
-T).(subst0 i v t2 t)))))))))).(\lambda (k: K).(\lambda (t2: T).(\lambda (t3: 
-T).(\lambda (H2: (subst0 (s k i) v t2 t3)).(\lambda (H3: ((\forall (t4: 
-T).(\forall (u3: T).(\forall (i2: nat).((subst0 i2 u3 t2 t4) \to ((not (eq 
-nat (s k i) i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u3 t3 t)) (\lambda (t: 
-T).(subst0 (s k i) v t4 t)))))))))).(\lambda (t4: T).(\lambda (u3: 
-T).(\lambda (i2: nat).(\lambda (H4: (subst0 i2 u3 (THead k u0 t2) 
-t4)).(\lambda (H5: (not (eq nat i i2))).(or3_ind (ex2 T (\lambda (u4: T).(eq 
-T t4 (THead k u4 t2))) (\lambda (u4: T).(subst0 i2 u3 u0 u4))) (ex2 T 
+(H1 x1 u2 (s k i2) H7 (ex2_ind T (\lambda (t: T).(subst0 (s k i2) u2 t2 t)) 
+(\lambda (t: T).(subst0 (s k i) v x1 t)) ((eq nat (s k i) (s k i2)) \to 
+False) (\lambda (x: T).(\lambda (_: (subst0 (s k i2) u2 t2 x)).(\lambda (_: 
+(subst0 (s k i) v x1 x)).(\lambda (H10: (eq nat (s k i) (s k i2))).(H3 (s_inj 
+k i i2 H10)))))) (H1 x1 u2 (s k i2) H7 (\lambda (H8: (eq nat (s k i) (s k 
+i2))).(H3 (s_inj k i i2 H8))))))) t4 H5)))))) H4)) (subst0_gen_head k u2 u t3 
+t4 i2 H2))))))))))))))) (\lambda (v: T).(\lambda (u0: T).(\lambda (u2: 
+T).(\lambda (i: nat).(\lambda (H0: (subst0 i v u0 u2)).(\lambda (H1: 
+((\forall (t2: T).(\forall (u3: T).(\forall (i2: nat).((subst0 i2 u3 u0 t2) 
+\to ((not (eq nat i i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u3 u2 t)) 
+(\lambda (t: T).(subst0 i v t2 t)))))))))).(\lambda (k: K).(\lambda (t2: 
+T).(\lambda (t3: T).(\lambda (H2: (subst0 (s k i) v t2 t3)).(\lambda (H3: 
+((\forall (t4: T).(\forall (u3: T).(\forall (i2: nat).((subst0 i2 u3 t2 t4) 
+\to ((not (eq nat (s k i) i2)) \to (ex2 T (\lambda (t: T).(subst0 i2 u3 t3 
+t)) (\lambda (t: T).(subst0 (s k i) v t4 t)))))))))).(\lambda (t4: 
+T).(\lambda (u3: T).(\lambda (i2: nat).(\lambda (H4: (subst0 i2 u3 (THead k 
+u0 t2) t4)).(\lambda (H5: (not (eq nat i i2))).(or3_ind (ex2 T (\lambda (u4: 
+T).(eq T t4 (THead k u4 t2))) (\lambda (u4: T).(subst0 i2 u3 u0 u4))) (ex2 T 
 (\lambda (t5: T).(eq T t4 (THead k u0 t5))) (\lambda (t5: T).(subst0 (s k i2) 
 u3 t2 t5))) (ex3_2 T T (\lambda (u4: T).(\lambda (t5: T).(eq T t4 (THead k u4 
 t5)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: 
@@ -460,31 +468,40 @@ T).(subst0 i2 u3 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i v t t5))))
 x0)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda 
 (t: T).(subst0 i v (THead k u0 x) t)) (THead k u2 x0) (subst0_snd k u3 x0 t3 
 i2 H9 u2) (subst0_both v u0 u2 i H0 k x x0 H10))))) (H3 x u3 (s k i2) H8 
-(\lambda (H9: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 H9))))) t4 H7)))) 
-H6)) (\lambda (H6: (ex3_2 T T (\lambda (u4: T).(\lambda (t5: T).(eq T t4 
+(ex2_ind T (\lambda (t: T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: T).(subst0 
+(s k i) v x t)) ((eq nat (s k i) (s k i2)) \to False) (\lambda (x0: 
+T).(\lambda (_: (subst0 (s k i2) u3 t3 x0)).(\lambda (_: (subst0 (s k i) v x 
+x0)).(\lambda (H11: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 H11)))))) 
+(H3 x u3 (s k i2) H8 (\lambda (H9: (eq nat (s k i) (s k i2))).(H5 (s_inj k i 
+i2 H9))))))) t4 H7)))) H6)) (\lambda (H6: (ex3_2 T T (\lambda (u4: 
+T).(\lambda (t5: T).(eq T t4 (THead k u4 t5)))) (\lambda (u4: T).(\lambda (_: 
+T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) 
+u3 t2 t5))))).(ex3_2_ind T T (\lambda (u4: T).(\lambda (t5: T).(eq T t4 
 (THead k u4 t5)))) (\lambda (u4: T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) 
-(\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) u3 t2 t5))))).(ex3_2_ind T 
-T (\lambda (u4: T).(\lambda (t5: T).(eq T t4 (THead k u4 t5)))) (\lambda (u4: 
-T).(\lambda (_: T).(subst0 i2 u3 u0 u4))) (\lambda (_: T).(\lambda (t5: 
-T).(subst0 (s k i2) u3 t2 t5))) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k 
-u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t))) (\lambda (x0: T).(\lambda (x1: 
-T).(\lambda (H7: (eq T t4 (THead k x0 x1))).(\lambda (H8: (subst0 i2 u3 u0 
-x0)).(\lambda (H9: (subst0 (s k i2) u3 t2 x1)).(eq_ind_r T (THead k x0 x1) 
-(\lambda (t: T).(ex2 T (\lambda (t5: T).(subst0 i2 u3 (THead k u2 t3) t5)) 
-(\lambda (t5: T).(subst0 i v t t5)))) (ex2_ind T (\lambda (t: T).(subst0 i2 
-u3 u2 t)) (\lambda (t: T).(subst0 i v x0 t)) (ex2 T (\lambda (t: T).(subst0 
-i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t))) 
-(\lambda (x: T).(\lambda (H10: (subst0 i2 u3 u2 x)).(\lambda (H11: (subst0 i 
-v x0 x)).(ex2_ind T (\lambda (t: T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: 
-T).(subst0 (s k i) v x1 t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 
-t3) t)) (\lambda (t: T).(subst0 i v (THead k x0 x1) t))) (\lambda (x2: 
-T).(\lambda (H12: (subst0 (s k i2) u3 t3 x2)).(\lambda (H13: (subst0 (s k i) 
-v x1 x2)).(ex_intro2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) 
-(\lambda (t: T).(subst0 i v (THead k x0 x1) t)) (THead k x x2) (subst0_both 
-u3 u2 x i2 H10 k t3 x2 H12) (subst0_both v x0 x i H11 k x1 x2 H13))))) (H3 x1 
-u3 (s k i2) H9 (\lambda (H12: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 
-H12)))))))) (H1 x0 u3 i2 H8 H5)) t4 H7)))))) H6)) (subst0_gen_head k u3 u0 t2 
-t4 i2 H4)))))))))))))))))) i1 u1 t0 t1 H))))).
+(\lambda (_: T).(\lambda (t5: T).(subst0 (s k i2) u3 t2 t5))) (ex2 T (\lambda 
+(t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v t4 t))) 
+(\lambda (x0: T).(\lambda (x1: T).(\lambda (H7: (eq T t4 (THead k x0 
+x1))).(\lambda (H8: (subst0 i2 u3 u0 x0)).(\lambda (H9: (subst0 (s k i2) u3 
+t2 x1)).(eq_ind_r T (THead k x0 x1) (\lambda (t: T).(ex2 T (\lambda (t5: 
+T).(subst0 i2 u3 (THead k u2 t3) t5)) (\lambda (t5: T).(subst0 i v t t5)))) 
+(ex2_ind T (\lambda (t: T).(subst0 i2 u3 u2 t)) (\lambda (t: T).(subst0 i v 
+x0 t)) (ex2 T (\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: 
+T).(subst0 i v (THead k x0 x1) t))) (\lambda (x: T).(\lambda (H10: (subst0 i2 
+u3 u2 x)).(\lambda (H11: (subst0 i v x0 x)).(ex2_ind T (\lambda (t: 
+T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: T).(subst0 (s k i) v x1 t)) (ex2 T 
+(\lambda (t: T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v 
+(THead k x0 x1) t))) (\lambda (x2: T).(\lambda (H12: (subst0 (s k i2) u3 t3 
+x2)).(\lambda (H13: (subst0 (s k i) v x1 x2)).(ex_intro2 T (\lambda (t: 
+T).(subst0 i2 u3 (THead k u2 t3) t)) (\lambda (t: T).(subst0 i v (THead k x0 
+x1) t)) (THead k x x2) (subst0_both u3 u2 x i2 H10 k t3 x2 H12) (subst0_both 
+v x0 x i H11 k x1 x2 H13))))) (H3 x1 u3 (s k i2) H9 (ex2_ind T (\lambda (t: 
+T).(subst0 (s k i2) u3 t3 t)) (\lambda (t: T).(subst0 (s k i) v x1 t)) ((eq 
+nat (s k i) (s k i2)) \to False) (\lambda (x2: T).(\lambda (_: (subst0 (s k 
+i2) u3 t3 x2)).(\lambda (_: (subst0 (s k i) v x1 x2)).(\lambda (H14: (eq nat 
+(s k i) (s k i2))).(H5 (s_inj k i i2 H14)))))) (H3 x1 u3 (s k i2) H9 (\lambda 
+(H12: (eq nat (s k i) (s k i2))).(H5 (s_inj k i i2 H12)))))))))) (H1 x0 u3 i2 
+H8 H5)) t4 H7)))))) H6)) (subst0_gen_head k u3 u0 t2 t4 i2 
+H4)))))))))))))))))) i1 u1 t0 t1 H))))).
 
 theorem subst0_confluence_eq:
  \forall (t0: T).(\forall (t1: T).(\forall (u: T).(\forall (i: nat).((subst0 
@@ -498,9 +515,9 @@ T).(\lambda (t2: T).(\lambda (t3: T).(\forall (t4: T).((subst0 n t t2 t4) \to
 (or4 (eq T t3 t4) (ex2 T (\lambda (t5: T).(subst0 n t t3 t5)) (\lambda (t5: 
 T).(subst0 n t t4 t5))) (subst0 n t t3 t4) (subst0 n t t4 t3)))))))) (\lambda 
 (v: T).(\lambda (i0: nat).(\lambda (t2: T).(\lambda (H0: (subst0 i0 v (TLRef 
-i0) t2)).(and_ind (eq nat i0 i0) (eq T t2 (lift (S i0) O v)) (or4 (eq T (lift 
-(S i0) O v) t2) (ex2 T (\lambda (t: T).(subst0 i0 v (lift (S i0) O v) t)) 
-(\lambda (t: T).(subst0 i0 v t2 t))) (subst0 i0 v (lift (S i0) O v) t2) 
+i0) t2)).(land_ind (eq nat i0 i0) (eq T t2 (lift (S i0) O v)) (or4 (eq T 
+(lift (S i0) O v) t2) (ex2 T (\lambda (t: T).(subst0 i0 v (lift (S i0) O v) 
+t)) (\lambda (t: T).(subst0 i0 v t2 t))) (subst0 i0 v (lift (S i0) O v) t2) 
 (subst0 i0 v t2 (lift (S i0) O v))) (\lambda (_: (eq nat i0 i0)).(\lambda 
 (H2: (eq T t2 (lift (S i0) O v))).(or4_intro0 (eq T (lift (S i0) O v) t2) 
 (ex2 T (\lambda (t: T).(subst0 i0 v (lift (S i0) O v) t)) (\lambda (t: 
@@ -1360,13 +1377,13 @@ i t1) t)) (eq T t1 t2) (\lambda (x: T).(\lambda (_: (subst0 i u (lift (S O) i
 t2) x)).(\lambda (H3: (subst0 i u (lift (S O) i t1) 
 x)).(subst0_gen_lift_false t1 u x (S O) i i (le_n i) (eq_ind_r nat (plus (S 
 O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O) i)) (plus i (S O)) 
-(plus_comm i (S O))) H3 (eq T t1 t2))))) H1)) (\lambda (H1: (subst0 i u (lift 
+(plus_sym i (S O))) H3 (eq T t1 t2))))) H1)) (\lambda (H1: (subst0 i u (lift 
 (S O) i t2) (lift (S O) i t1))).(subst0_gen_lift_false t2 u (lift (S O) i t1) 
 (S O) i i (le_n i) (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(lt i n)) 
-(le_n (plus (S O) i)) (plus i (S O)) (plus_comm i (S O))) H1 (eq T t1 t2))) 
+(le_n (plus (S O) i)) (plus i (S O)) (plus_sym i (S O))) H1 (eq T t1 t2))) 
 (\lambda (H1: (subst0 i u (lift (S O) i t1) (lift (S O) i 
 t2))).(subst0_gen_lift_false t1 u (lift (S O) i t2) (S O) i i (le_n i) 
 (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(lt i n)) (le_n (plus (S O) 
-i)) (plus i (S O)) (plus_comm i (S O))) H1 (eq T t1 t2))) 
+i)) (plus i (S O)) (plus_sym i (S O))) H1 (eq T t1 t2))) 
 (subst0_confluence_eq t0 (lift (S O) i t2) u i H0 (lift (S O) i t1) H)))))))).