set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt".
-include "lift/defs.ma".
+include "lift/fwd.ma".
-include "tlt/defs.ma".
+include "tlt/props.ma".
theorem lift_weight_map:
\forall (t: T).(\forall (h: nat).(\forall (d: nat).(\forall (f: ((nat \to
(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
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)
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