Procedural : tentative update to the new letin cic construction

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma
index 168d3e09c18bf7d109e3aeb21421c15cb5093126..20649f9bf4357b641e5c0495d29814207c967d4d 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma
@@ -105,7 +105,7 @@ theorem lift_lref_gt:
 (plus (pred n) (S O))) (\lambda (t: T).(eq T t (TLRef n))) (eq_ind nat (plus 
 (S O) (pred n)) (\lambda (n0: nat).(eq T (TLRef n0) (TLRef n))) (eq_ind nat n 
 (\lambda (n0: nat).(eq T (TLRef n0) (TLRef n))) (refl_equal T (TLRef n)) (S 
-(pred n)) (S_pred n d H)) (plus (pred n) (S O)) (plus_comm (S O) (pred n))) 
+(pred n)) (S_pred n d H)) (plus (pred n) (S O)) (plus_sym (S O) (pred n))) 
 (lift (S O) d (TLRef (pred n))) (lift_lref_ge (pred n) (S O) d (le_S_n d 
 (pred n) (eq_ind nat n (\lambda (n0: nat).(le (S d) n0)) H (S (pred n)) 
 (S_pred n d H))))))).
@@ -234,30 +234,30 @@ n) (eq_ind_r T (TLRef (plus n h1)) (\lambda (t: T).(eq T (TLRef (plus n h1))
 t)) (refl_equal T (TLRef (plus n h1))) (lift h1 d1 (TLRef n)) (lift_lref_ge n 
 h1 d1 H1)) (eq_ind_r T (TLRef n) (\lambda (t: T).(eq T (TLRef n) t)) 
 (refl_equal T (TLRef n)) (lift h2 d2 (TLRef n)) (lift_lref_lt n h2 d2 H3))) x 
-(lift_gen_lref_lt h2 (plus d2 h1) (plus n h1) (plus_lt_compat_r n d2 h1 H3) x 
-H2))) (\lambda (H3: (le d2 n)).(lt_le_e n (plus d2 h2) (ex2 T (\lambda (t2: 
-T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 
-t2)))) (\lambda (H4: (lt n (plus d2 h2))).(lift_gen_lref_false h2 (plus d2 
-h1) (plus n h1) (plus_le_compat d2 n h1 h1 H3 (le_n h1)) (eq_ind_r nat (plus 
-(plus d2 h2) h1) (\lambda (n0: nat).(lt (plus n h1) n0)) (plus_lt_compat_r n 
-(plus d2 h2) h1 H4) (plus (plus d2 h1) h2) (plus_permute_2_in_3 d2 h1 h2)) x 
-H2 (ex2 T (\lambda (t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T 
-(TLRef n) (lift h2 d2 t2)))))) (\lambda (H4: (le (plus d2 h2) n)).(let H5 
-\def (eq_ind nat (plus n h1) (\lambda (n0: nat).(eq T (TLRef n0) (lift h2 
-(plus d2 h1) x))) H2 (plus (minus (plus n h1) h2) h2) (le_plus_minus_sym h2 
-(plus n h1) (le_plus_trans h2 n h1 (le_trans h2 (plus d2 h2) n (le_plus_r d2 
-h2) H4)))) in (eq_ind_r T (TLRef (minus (plus n h1) h2)) (\lambda (t: T).(ex2 
-T (\lambda (t2: T).(eq T t (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) 
-(lift h2 d2 t2))))) (ex_intro2 T (\lambda (t2: T).(eq T (TLRef (minus (plus n 
-h1) h2)) (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))) 
-(TLRef (minus n h2)) (eq_ind_r nat (plus (minus n h2) h1) (\lambda (n0: 
-nat).(eq T (TLRef n0) (lift h1 d1 (TLRef (minus n h2))))) (eq_ind_r T (TLRef 
-(plus (minus n h2) h1)) (\lambda (t: T).(eq T (TLRef (plus (minus n h2) h1)) 
-t)) (refl_equal T (TLRef (plus (minus n h2) h1))) (lift h1 d1 (TLRef (minus n 
-h2))) (lift_lref_ge (minus n h2) h1 d1 (le_trans d1 d2 (minus n h2) H 
-(le_minus d2 n h2 H4)))) (minus (plus n h1) h2) (le_minus_plus h2 n (le_trans 
-h2 (plus d2 h2) n (le_plus_r d2 h2) H4) h1)) (eq_ind_r nat (plus (minus n h2) 
-h2) (\lambda (n0: nat).(eq T (TLRef n0) (lift h2 d2 (TLRef (minus n0 h2))))) 
+(lift_gen_lref_lt h2 (plus d2 h1) (plus n h1) (lt_reg_r n d2 h1 H3) x H2))) 
+(\lambda (H3: (le d2 n)).(lt_le_e n (plus d2 h2) (ex2 T (\lambda (t2: T).(eq 
+T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2)))) 
+(\lambda (H4: (lt n (plus d2 h2))).(lift_gen_lref_false h2 (plus d2 h1) (plus 
+n h1) (le_plus_plus d2 n h1 h1 H3 (le_n h1)) (eq_ind_r nat (plus (plus d2 h2) 
+h1) (\lambda (n0: nat).(lt (plus n h1) n0)) (lt_reg_r n (plus d2 h2) h1 H4) 
+(plus (plus d2 h1) h2) (plus_permute_2_in_3 d2 h1 h2)) x H2 (ex2 T (\lambda 
+(t2: T).(eq T x (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 
+d2 t2)))))) (\lambda (H4: (le (plus d2 h2) n)).(let H5 \def (eq_ind nat (plus 
+n h1) (\lambda (n0: nat).(eq T (TLRef n0) (lift h2 (plus d2 h1) x))) H2 (plus 
+(minus (plus n h1) h2) h2) (le_plus_minus_sym h2 (plus n h1) (le_plus_trans 
+h2 n h1 (le_trans h2 (plus d2 h2) n (le_plus_r d2 h2) H4)))) in (eq_ind_r T 
+(TLRef (minus (plus n h1) h2)) (\lambda (t: T).(ex2 T (\lambda (t2: T).(eq T 
+t (lift h1 d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))))) 
+(ex_intro2 T (\lambda (t2: T).(eq T (TLRef (minus (plus n h1) h2)) (lift h1 
+d1 t2))) (\lambda (t2: T).(eq T (TLRef n) (lift h2 d2 t2))) (TLRef (minus n 
+h2)) (eq_ind_r nat (plus (minus n h2) h1) (\lambda (n0: nat).(eq T (TLRef n0) 
+(lift h1 d1 (TLRef (minus n h2))))) (eq_ind_r T (TLRef (plus (minus n h2) 
+h1)) (\lambda (t: T).(eq T (TLRef (plus (minus n h2) h1)) t)) (refl_equal T 
+(TLRef (plus (minus n h2) h1))) (lift h1 d1 (TLRef (minus n h2))) 
+(lift_lref_ge (minus n h2) h1 d1 (le_trans d1 d2 (minus n h2) H (le_minus d2 
+n h2 H4)))) (minus (plus n h1) h2) (le_minus_plus h2 n (le_trans h2 (plus d2 
+h2) n (le_plus_r d2 h2) H4) h1)) (eq_ind_r nat (plus (minus n h2) h2) 
+(\lambda (n0: nat).(eq T (TLRef n0) (lift h2 d2 (TLRef (minus n0 h2))))) 
 (eq_ind_r T (TLRef (plus (minus (plus (minus n h2) h2) h2) h2)) (\lambda (t: 
 T).(eq T (TLRef (plus (minus n h2) h2)) t)) (f_equal nat T TLRef (plus (minus 
 n h2) h2) (plus (minus (plus (minus n h2) h2) h2) h2) (f_equal2 nat nat nat 
@@ -265,8 +265,8 @@ plus (minus n h2) (minus (plus (minus n h2) h2) h2) h2 h2 (sym_eq nat (minus
 (plus (minus n h2) h2) h2) (minus n h2) (minus_plus_r (minus n h2) h2)) 
 (refl_equal nat h2))) (lift h2 d2 (TLRef (minus (plus (minus n h2) h2) h2))) 
 (lift_lref_ge (minus (plus (minus n h2) h2) h2) h2 d2 (le_minus d2 (plus 
-(minus n h2) h2) h2 (plus_le_compat d2 (minus n h2) h2 h2 (le_minus d2 n h2 
-H4) (le_n h2))))) n (le_plus_minus_sym h2 n (le_trans h2 (plus d2 h2) n 
+(minus n h2) h2) h2 (le_plus_plus d2 (minus n h2) h2 h2 (le_minus d2 n h2 H4) 
+(le_n h2))))) n (le_plus_minus_sym h2 n (le_trans h2 (plus d2 h2) n 
 (le_plus_r d2 h2) H4)))) x (lift_gen_lref_ge h2 (plus d2 h1) (minus (plus n 
 h1) h2) (arith0 h2 d2 n H4 h1) x H5)))))))))))))))))) (\lambda (k: 
 K).(\lambda (t: T).(\lambda (H: ((\forall (x: T).(\forall (h1: nat).(\forall 
@@ -411,7 +411,7 @@ n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: T).(eq T (lift k e t0) (lift
 nat T TLRef (plus (plus n h) k) (plus n (plus k h)) 
 (plus_permute_2_in_3_assoc n h k)) (lift (plus k h) d (TLRef n)) 
 (lift_lref_ge n (plus k h) d H1)) (lift k e (TLRef (plus n h))) (lift_lref_ge 
-(plus n h) k e (le_trans e (plus d h) (plus n h) H (plus_le_compat d n h h H1 
+(plus n h) k e (le_trans e (plus d h) (plus n h) H (le_plus_plus d n h h H1 
 (le_n h))))) (lift h d (TLRef n)) (lift_lref_ge n h d H1))))))))))) (\lambda 
 (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (k0: 
 nat).(\forall (d: nat).(\forall (e: nat).((le e (plus d h)) \to ((le d e) \to 
@@ -474,17 +474,17 @@ nat).(eq T (lift h n0 (TLRef (plus n k))) (lift k e (lift h d (TLRef n)))))
 (plus n k)) (\lambda (t0: T).(eq T (TLRef (plus n k)) t0)) (refl_equal T 
 (TLRef (plus n k))) (lift k e (TLRef n)) (lift_lref_ge n k e H0)) (lift h d 
 (TLRef n)) (lift_lref_lt n h d H1)) (lift h (plus d k) (TLRef (plus n k))) 
-(lift_lref_lt (plus n k) h (plus d k) (plus_lt_compat_r n d k H1)))) (\lambda 
-(H1: (le d n)).(eq_ind_r T (TLRef (plus (plus n k) h)) (\lambda (t0: T).(eq T 
-t0 (lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef (plus n h)) (\lambda 
+(lift_lref_lt (plus n k) h (plus d k) (lt_reg_r n d k H1)))) (\lambda (H1: 
+(le d n)).(eq_ind_r T (TLRef (plus (plus n k) h)) (\lambda (t0: T).(eq T t0 
+(lift k e (lift h d (TLRef n))))) (eq_ind_r T (TLRef (plus n h)) (\lambda 
 (t0: T).(eq T (TLRef (plus (plus n k) h)) (lift k e t0))) (eq_ind_r T (TLRef 
 (plus (plus n h) k)) (\lambda (t0: T).(eq T (TLRef (plus (plus n k) h)) t0)) 
 (f_equal nat T TLRef (plus (plus n k) h) (plus (plus n h) k) (sym_eq nat 
 (plus (plus n h) k) (plus (plus n k) h) (plus_permute_2_in_3 n h k))) (lift k 
 e (TLRef (plus n h))) (lift_lref_ge (plus n h) k e (le_plus_trans e n h H0))) 
 (lift h d (TLRef n)) (lift_lref_ge n h d H1)) (lift h (plus d k) (TLRef (plus 
-n k))) (lift_lref_ge (plus n k) h (plus d k) (plus_le_compat d n k k H1 (le_n 
-k)))))) (plus k d) (plus_comm k d)) (lift k e (TLRef n)) (lift_lref_ge n k e 
+n k))) (lift_lref_ge (plus n k) h (plus d k) (le_plus_plus d n k k H1 (le_n 
+k)))))) (plus k d) (plus_sym k d)) (lift k e (TLRef n)) (lift_lref_ge n k e 
 H0)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (H: ((\forall (h: 
 nat).(\forall (k0: nat).(\forall (d: nat).(\forall (e: nat).((le e d) \to (eq 
 T (lift h (plus k0 d) (lift k0 e t0)) (lift k0 e (lift h d