last problem elegantly resolved!

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma
index b67722f58eca72d17f85f8253d96291c8a825580..f03f26618fb665260145b2ab6b126194b36209eb 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma
@@ -141,14 +141,14 @@ d) \to (eq nat (g m) (f m)))))).(\lambda (_: (eq nat (g d) w)).(\lambda (H1:
 (TLRef n)))) (\lambda (H2: (lt n d)).(eq_ind_r T (TLRef n) (\lambda (t0: 
 T).(eq nat (weight_map f t0) (weight_map g (lift (S h) d (TLRef n))))) 
 (eq_ind_r T (TLRef n) (\lambda (t0: T).(eq nat (weight_map f (TLRef n)) 
-(weight_map g t0))) (sym_equal nat (g n) (f n) (H n H2)) (lift (S h) d (TLRef 
+(weight_map g t0))) (sym_eq nat (g n) (f n) (H n H2)) (lift (S h) d (TLRef 
 n)) (lift_lref_lt n (S h) d H2)) (lift h d (TLRef n)) (lift_lref_lt n h d 
 H2))) (\lambda (H2: (le d n)).(eq_ind_r T (TLRef (plus n h)) (\lambda (t0: 
 T).(eq nat (weight_map f t0) (weight_map g (lift (S h) d (TLRef n))))) 
 (eq_ind_r T (TLRef (plus n (S h))) (\lambda (t0: T).(eq nat (weight_map f 
 (TLRef (plus n h))) (weight_map g t0))) (eq_ind nat (S (plus n h)) (\lambda 
-(n0: nat).(eq nat (f (plus n h)) (g n0))) (sym_equal nat (g (S (plus n h))) 
-(f (plus n h)) (H1 (plus n h) (le_plus_trans d n h H2))) (plus n (S h)) 
+(n0: nat).(eq nat (f (plus n h)) (g n0))) (sym_eq nat (g (S (plus n h))) (f 
+(plus n h)) (H1 (plus n h) (le_plus_trans d n h H2))) (plus n (S h)) 
 (plus_n_Sm n h)) (lift (S h) d (TLRef n)) (lift_lref_ge n (S h) d H2)) (lift 
 h d (TLRef n)) (lift_lref_ge n h d H2)))))))))))) (\lambda (k: K).(\lambda 
 (t0: T).(\lambda (H: ((\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat 
@@ -195,32 +195,51 @@ d))).(or_ind (eq nat m O) (ex2 nat (\lambda (m0: nat).(eq nat m (S m0)))
 t0))) m) (wadd f (S (weight_map f (lift h d t0))) m)) (\lambda (H5: (eq nat m 
 O)).(eq_ind_r nat O (\lambda (n: nat).(eq nat (wadd g (S (weight_map g (lift 
 (S h) d t0))) n) (wadd f (S (weight_map f (lift h d t0))) n))) (f_equal nat 
-nat S (weight_map g (lift (S h) d t0)) (weight_map f (lift h d t0)) 
-(sym_equal nat (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0)) 
-(H h d f g H1 H2 H3))) m H5)) (\lambda (H5: (ex2 nat (\lambda (m0: nat).(eq 
-nat m (S m0))) (\lambda (m: nat).(lt m d)))).(ex2_ind nat (\lambda (m0: 
-nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g (S 
-(weight_map g (lift (S h) d t0))) m) (wadd f (S (weight_map f (lift h d t0))) 
-m)) (\lambda (x: nat).(\lambda (H6: (eq nat m (S x))).(\lambda (H7: (lt x 
-d)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd g (S (weight_map g 
-(lift (S h) d t0))) n) (wadd f (S (weight_map f (lift h d t0))) n))) (H1 x 
-H7) m H6)))) H5)) (lt_gen_xS m d H4)))) H2 (\lambda (m: nat).(\lambda (H4: 
-(le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: 
-nat).(le d n)) (eq nat (g m) (wadd f (S (weight_map f (lift h d t0))) m)) 
-(\lambda (x: nat).(\lambda (H5: (eq nat m (S x))).(\lambda (H6: (le d 
-x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (g n) (wadd f (S 
-(weight_map f (lift h d t0))) n))) (H3 x H6) m H5)))) (le_gen_S d m H4))))))) 
-(f_equal nat nat S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) 
-(lift h (S d) t1))) (plus (weight_map g (lift (S h) d t0)) (weight_map (wadd 
-g O) (lift (S h) (S d) t1))) (f_equal2 nat nat nat plus (weight_map f (lift h 
-d t0)) (weight_map g (lift (S h) d t0)) (weight_map (wadd f O) (lift h (S d) 
-t1)) (weight_map (wadd g O) (lift (S h) (S d) t1)) (H h d f g H1 H2 H3) (H0 h 
-(S d) (wadd f O) (wadd g O) (\lambda (m: nat).(\lambda (H4: (lt m (S 
+nat S (weight_map g (lift (S h) d t0)) (weight_map f (lift h d t0)) (sym_eq 
+nat (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0)) (H h d f g 
+H1 H2 H3))) m H5)) (\lambda (H5: (ex2 nat (\lambda (m0: nat).(eq nat m (S 
+m0))) (\lambda (m0: nat).(lt m0 d)))).(ex2_ind nat (\lambda (m0: nat).(eq nat 
+m (S m0))) (\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g (S (weight_map g 
+(lift (S h) d t0))) m) (wadd f (S (weight_map f (lift h d t0))) m)) (\lambda 
+(x: nat).(\lambda (H6: (eq nat m (S x))).(\lambda (H7: (lt x d)).(eq_ind_r 
+nat (S x) (\lambda (n: nat).(eq nat (wadd g (S (weight_map g (lift (S h) d 
+t0))) n) (wadd f (S (weight_map f (lift h d t0))) n))) (H1 x H7) m H6)))) 
+H5)) (lt_gen_xS m d H4)))) H2 (\lambda (m: nat).(\lambda (H4: (le (S d) 
+m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d 
+n)) (eq nat (g m) (wadd f (S (weight_map f (lift h d t0))) m)) (\lambda (x: 
+nat).(\lambda (H5: (eq nat m (S x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S 
+x) (\lambda (n: nat).(eq nat (g n) (wadd f (S (weight_map f (lift h d t0))) 
+n))) (H3 x H6) m H5)))) (le_gen_S d m H4))))))) (f_equal nat nat S (plus 
+(weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d) t1))) (plus 
+(weight_map g (lift (S h) d t0)) (weight_map (wadd g O) (lift (S h) (S d) 
+t1))) (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) (weight_map g 
+(lift (S h) d t0)) (weight_map (wadd f O) (lift h (S d) t1)) (weight_map 
+(wadd g O) (lift (S h) (S d) t1)) (H h d f g H1 H2 H3) (H0 h (S d) (wadd f O) 
+(wadd g O) (\lambda (m: nat).(\lambda (H4: (lt m (S d))).(or_ind (eq nat m O) 
+(ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d))) 
+(eq nat (wadd g O m) (wadd f O m)) (\lambda (H5: (eq nat m O)).(eq_ind_r nat 
+O (\lambda (n: nat).(eq nat (wadd g O n) (wadd f O n))) (refl_equal nat O) m 
+H5)) (\lambda (H5: (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda 
+(m0: nat).(lt m0 d)))).(ex2_ind nat (\lambda (m0: nat).(eq nat m (S m0))) 
+(\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g O m) (wadd f O m)) (\lambda (x: 
+nat).(\lambda (H6: (eq nat m (S x))).(\lambda (H7: (lt x d)).(eq_ind_r nat (S 
+x) (\lambda (n: nat).(eq nat (wadd g O n) (wadd f O n))) (H1 x H7) m H6)))) 
+H5)) (lt_gen_xS m d H4)))) H2 (\lambda (m: nat).(\lambda (H4: (le (S d) 
+m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d 
+n)) (eq nat (g m) (wadd f O m)) (\lambda (x: nat).(\lambda (H5: (eq nat m (S 
+x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (g 
+n) (wadd f O n))) (H3 x H6) m H5)))) (le_gen_S d m H4))))))) (f_equal nat nat 
+S (plus (weight_map f (lift h d t0)) (weight_map (wadd f O) (lift h (S d) 
+t1))) (plus (weight_map g (lift (S h) d t0)) (weight_map (wadd g O) (lift (S 
+h) (S d) t1))) (f_equal2 nat nat nat plus (weight_map f (lift h d t0)) 
+(weight_map g (lift (S h) d t0)) (weight_map (wadd f O) (lift h (S d) t1)) 
+(weight_map (wadd g O) (lift (S h) (S d) t1)) (H h d f g H1 H2 H3) (H0 h (S 
+d) (wadd f O) (wadd g O) (\lambda (m: nat).(\lambda (H4: (lt m (S 
 d))).(or_ind (eq nat m O) (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) 
 (\lambda (m0: nat).(lt m0 d))) (eq nat (wadd g O m) (wadd f O m)) (\lambda 
 (H5: (eq nat m O)).(eq_ind_r nat O (\lambda (n: nat).(eq nat (wadd g O n) 
 (wadd f O n))) (refl_equal nat O) m H5)) (\lambda (H5: (ex2 nat (\lambda (m0: 
-nat).(eq nat m (S m0))) (\lambda (m: nat).(lt m d)))).(ex2_ind nat (\lambda 
+nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)))).(ex2_ind nat (\lambda 
 (m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d)) (eq nat (wadd g O 
 m) (wadd f O m)) (\lambda (x: nat).(\lambda (H6: (eq nat m (S x))).(\lambda 
 (H7: (lt x d)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (wadd g O n) 
@@ -229,40 +248,21 @@ nat).(\lambda (H4: (le (S d) m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S
 n))) (\lambda (n: nat).(le d n)) (eq nat (g m) (wadd f O m)) (\lambda (x: 
 nat).(\lambda (H5: (eq nat m (S x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S 
 x) (\lambda (n: nat).(eq nat (g n) (wadd f O n))) (H3 x H6) m H5)))) 
-(le_gen_S d m H4))))))) (f_equal nat nat S (plus (weight_map f (lift h d t0)) 
-(weight_map (wadd f O) (lift h (S d) t1))) (plus (weight_map g (lift (S h) d 
-t0)) (weight_map (wadd g O) (lift (S h) (S d) t1))) (f_equal2 nat nat nat 
-plus (weight_map f (lift h d t0)) (weight_map g (lift (S h) d t0)) 
-(weight_map (wadd f O) (lift h (S d) t1)) (weight_map (wadd g O) (lift (S h) 
-(S d) t1)) (H h d f g H1 H2 H3) (H0 h (S d) (wadd f O) (wadd g O) (\lambda 
-(m: nat).(\lambda (H4: (lt m (S d))).(or_ind (eq nat m O) (ex2 nat (\lambda 
-(m0: nat).(eq nat m (S m0))) (\lambda (m0: nat).(lt m0 d))) (eq nat (wadd g O 
-m) (wadd f O m)) (\lambda (H5: (eq nat m O)).(eq_ind_r nat O (\lambda (n: 
-nat).(eq nat (wadd g O n) (wadd f O n))) (refl_equal nat O) m H5)) (\lambda 
-(H5: (ex2 nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m: nat).(lt m 
-d)))).(ex2_ind nat (\lambda (m0: nat).(eq nat m (S m0))) (\lambda (m0: 
-nat).(lt m0 d)) (eq nat (wadd g O m) (wadd f O m)) (\lambda (x: nat).(\lambda 
-(H6: (eq nat m (S x))).(\lambda (H7: (lt x d)).(eq_ind_r nat (S x) (\lambda 
-(n: nat).(eq nat (wadd g O n) (wadd f O n))) (H1 x H7) m H6)))) H5)) 
-(lt_gen_xS m d H4)))) H2 (\lambda (m: nat).(\lambda (H4: (le (S d) 
-m)).(ex2_ind nat (\lambda (n: nat).(eq nat m (S n))) (\lambda (n: nat).(le d 
-n)) (eq nat (g m) (wadd f O m)) (\lambda (x: nat).(\lambda (H5: (eq nat m (S 
-x))).(\lambda (H6: (le d x)).(eq_ind_r nat (S x) (\lambda (n: nat).(eq nat (g 
-n) (wadd f O n))) (H3 x H6) m H5)))) (le_gen_S d m H4))))))) b) (lift (S h) d 
-(THead (Bind b) t0 t1)) (lift_head (Bind b) t0 t1 (S h) d)) (lift h d (THead 
-(Bind b) t0 t1)) (lift_head (Bind b) t0 t1 h d))) (\lambda (f0: F).(eq_ind_r 
-T (THead (Flat f0) (lift h d t0) (lift h (s (Flat f0) d) t1)) (\lambda (t2: 
-T).(eq nat (weight_map f t2) (weight_map g (lift (S h) d (THead (Flat f0) t0 
-t1))))) (eq_ind_r T (THead (Flat f0) (lift (S h) d t0) (lift (S h) (s (Flat 
-f0) d) t1)) (\lambda (t2: T).(eq nat (weight_map f (THead (Flat f0) (lift h d 
-t0) (lift h (s (Flat f0) d) t1))) (weight_map g t2))) (f_equal nat nat S 
-(plus (weight_map f (lift h d t0)) (weight_map f (lift h d t1))) (plus 
-(weight_map g (lift (S h) d t0)) (weight_map g (lift (S h) d t1))) (f_equal2 
-nat nat nat plus (weight_map f (lift h d t0)) (weight_map g (lift (S h) d 
-t0)) (weight_map f (lift h d t1)) (weight_map g (lift (S h) d t1)) (H h d f g 
-H1 H2 H3) (H0 h d f g H1 H2 H3))) (lift (S h) d (THead (Flat f0) t0 t1)) 
-(lift_head (Flat f0) t0 t1 (S h) d)) (lift h d (THead (Flat f0) t0 t1)) 
-(lift_head (Flat f0) t0 t1 h d))) k))))))))))))) t)).
+(le_gen_S d m H4))))))) b) (lift (S h) d (THead (Bind b) t0 t1)) (lift_head 
+(Bind b) t0 t1 (S h) d)) (lift h d (THead (Bind b) t0 t1)) (lift_head (Bind 
+b) t0 t1 h d))) (\lambda (f0: F).(eq_ind_r T (THead (Flat f0) (lift h d t0) 
+(lift h (s (Flat f0) d) t1)) (\lambda (t2: T).(eq nat (weight_map f t2) 
+(weight_map g (lift (S h) d (THead (Flat f0) t0 t1))))) (eq_ind_r T (THead 
+(Flat f0) (lift (S h) d t0) (lift (S h) (s (Flat f0) d) t1)) (\lambda (t2: 
+T).(eq nat (weight_map f (THead (Flat f0) (lift h d t0) (lift h (s (Flat f0) 
+d) t1))) (weight_map g t2))) (f_equal nat nat S (plus (weight_map f (lift h d 
+t0)) (weight_map f (lift h d t1))) (plus (weight_map g (lift (S h) d t0)) 
+(weight_map g (lift (S h) d t1))) (f_equal2 nat nat nat plus (weight_map f 
+(lift h d t0)) (weight_map g (lift (S h) d t0)) (weight_map f (lift h d t1)) 
+(weight_map g (lift (S h) d t1)) (H h d f g H1 H2 H3) (H0 h d f g H1 H2 H3))) 
+(lift (S h) d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 (S h) d)) 
+(lift h d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 h d))) 
+k))))))))))))) t)).
 
 theorem lift_weight_add_O:
  \forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (f: ((nat \to