Procedural : tentative update to the new letin cic construction

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma
index 3dbbd61477d1c6f5ff21157c10d3fab207a5b059..db188a2509d408206ac6df4acc03f979c10f2533 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma
@@ -144,7 +144,7 @@ i) t0)) H (TLRef (plus n h)) (lift_lref_ge n h d H0)) in (let H2 \def
 h)))) (land (le (plus d h) (plus n h)) (eq T (TLRef n) (TLRef n0))))) 
 (or_intror (land (lt (plus n h) d) (eq T (TLRef n) (TLRef (plus n h)))) (land 
 (le (plus d h) (plus n h)) (eq T (TLRef n) (TLRef n))) (conj (le (plus d h) 
-(plus n h)) (eq T (TLRef n) (TLRef n)) (plus_le_compat d n h h H0 (le_n h)) 
+(plus n h)) (eq T (TLRef n) (TLRef n)) (le_plus_plus d n h h H0 (le_n h)) 
 (refl_equal T (TLRef n)))) (minus (plus n h) h) (minus_plus_r n h)) i 
 H2)))))))))) (\lambda (k: K).(\lambda (t0: T).(\lambda (_: ((\forall (d: 
 nat).(\forall (h: nat).(\forall (i: nat).((eq T (TLRef i) (lift h d t0)) \to 
@@ -171,16 +171,16 @@ theorem lift_gen_lref_lt:
 d)).(\lambda (t: T).(\lambda (H0: (eq T (TLRef n) (lift h d t))).(let H_x 
 \def (lift_gen_lref t d h n H0) in (let H1 \def H_x in (or_ind (land (lt n d) 
 (eq T t (TLRef n))) (land (le (plus d h) n) (eq T t (TLRef (minus n h)))) (eq 
-T t (TLRef n)) (\lambda (H2: (land (lt n d) (eq T t (TLRef n)))).(and_ind (lt 
-n d) (eq T t (TLRef n)) (eq T t (TLRef n)) (\lambda (_: (lt n d)).(\lambda 
-(H4: (eq T t (TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: T).(eq T t0 
-(TLRef n))) (refl_equal T (TLRef n)) t H4))) H2)) (\lambda (H2: (land (le 
-(plus d h) n) (eq T t (TLRef (minus n h))))).(and_ind (le (plus d h) n) (eq T 
-t (TLRef (minus n h))) (eq T t (TLRef n)) (\lambda (H3: (le (plus d h) 
-n)).(\lambda (H4: (eq T t (TLRef (minus n h)))).(eq_ind_r T (TLRef (minus n 
-h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (le_false (plus d h) n (eq T (TLRef 
-(minus n h)) (TLRef n)) H3 (lt_le_S n (plus d h) (le_plus_trans (S n) d h 
-H))) t H4))) H2)) H1)))))))).
+T t (TLRef n)) (\lambda (H2: (land (lt n d) (eq T t (TLRef n)))).(land_ind 
+(lt n d) (eq T t (TLRef n)) (eq T t (TLRef n)) (\lambda (_: (lt n 
+d)).(\lambda (H4: (eq T t (TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: 
+T).(eq T t0 (TLRef n))) (refl_equal T (TLRef n)) t H4))) H2)) (\lambda (H2: 
+(land (le (plus d h) n) (eq T t (TLRef (minus n h))))).(land_ind (le (plus d 
+h) n) (eq T t (TLRef (minus n h))) (eq T t (TLRef n)) (\lambda (H3: (le (plus 
+d h) n)).(\lambda (H4: (eq T t (TLRef (minus n h)))).(eq_ind_r T (TLRef 
+(minus n h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (le_false (plus d h) n (eq 
+T (TLRef (minus n h)) (TLRef n)) H3 (lt_le_S n (plus d h) (le_plus_trans (S 
+n) d h H))) t H4))) H2)) H1)))))))).
 
 theorem lift_gen_lref_false:
  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to ((lt n 
@@ -192,12 +192,12 @@ n)).(\lambda (H0: (lt n (plus d h))).(\lambda (t: T).(\lambda (H1: (eq T
 (TLRef n) (lift h d t))).(\lambda (P: Prop).(let H_x \def (lift_gen_lref t d 
 h n H1) in (let H2 \def H_x in (or_ind (land (lt n d) (eq T t (TLRef n))) 
 (land (le (plus d h) n) (eq T t (TLRef (minus n h)))) P (\lambda (H3: (land 
-(lt n d) (eq T t (TLRef n)))).(and_ind (lt n d) (eq T t (TLRef n)) P (\lambda 
-(H4: (lt n d)).(\lambda (_: (eq T t (TLRef n))).(le_false d n P H H4))) H3)) 
-(\lambda (H3: (land (le (plus d h) n) (eq T t (TLRef (minus n h))))).(and_ind 
-(le (plus d h) n) (eq T t (TLRef (minus n h))) P (\lambda (H4: (le (plus d h) 
-n)).(\lambda (_: (eq T t (TLRef (minus n h)))).(le_false (plus d h) n P H4 
-H0))) H3)) H2)))))))))).
+(lt n d) (eq T t (TLRef n)))).(land_ind (lt n d) (eq T t (TLRef n)) P 
+(\lambda (H4: (lt n d)).(\lambda (_: (eq T t (TLRef n))).(le_false d n P H 
+H4))) H3)) (\lambda (H3: (land (le (plus d h) n) (eq T t (TLRef (minus n 
+h))))).(land_ind (le (plus d h) n) (eq T t (TLRef (minus n h))) P (\lambda 
+(H4: (le (plus d h) n)).(\lambda (_: (eq T t (TLRef (minus n h)))).(le_false 
+(plus d h) n P H4 H0))) H3)) H2)))))))))).
 
 theorem lift_gen_lref_ge:
  \forall (h: nat).(\forall (d: nat).(\forall (n: nat).((le d n) \to (\forall 
@@ -208,14 +208,14 @@ n)).(\lambda (t: T).(\lambda (H0: (eq T (TLRef (plus n h)) (lift h d
 t))).(let H_x \def (lift_gen_lref t d h (plus n h) H0) in (let H1 \def H_x in 
 (or_ind (land (lt (plus n h) d) (eq T t (TLRef (plus n h)))) (land (le (plus 
 d h) (plus n h)) (eq T t (TLRef (minus (plus n h) h)))) (eq T t (TLRef n)) 
-(\lambda (H2: (land (lt (plus n h) d) (eq T t (TLRef (plus n h))))).(and_ind 
+(\lambda (H2: (land (lt (plus n h) d) (eq T t (TLRef (plus n h))))).(land_ind 
 (lt (plus n h) d) (eq T t (TLRef (plus n h))) (eq T t (TLRef n)) (\lambda 
 (H3: (lt (plus n h) d)).(\lambda (H4: (eq T t (TLRef (plus n h)))).(eq_ind_r 
 T (TLRef (plus n h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (le_false d n (eq 
 T (TLRef (plus n h)) (TLRef n)) H (lt_le_S n d (simpl_lt_plus_r h n d 
 (lt_le_trans (plus n h) d (plus d h) H3 (le_plus_l d h))))) t H4))) H2)) 
 (\lambda (H2: (land (le (plus d h) (plus n h)) (eq T t (TLRef (minus (plus n 
-h) h))))).(and_ind (le (plus d h) (plus n h)) (eq T t (TLRef (minus (plus n 
+h) h))))).(land_ind (le (plus d h) (plus n h)) (eq T t (TLRef (minus (plus n 
 h) h))) (eq T t (TLRef n)) (\lambda (_: (le (plus d h) (plus n h))).(\lambda 
 (H4: (eq T t (TLRef (minus (plus n h) h)))).(eq_ind_r T (TLRef (minus (plus n 
 h) h)) (\lambda (t0: T).(eq T t0 (TLRef n))) (f_equal nat T TLRef (minus