(weight_map f (lift h d t1)) (weight_map f t1) (H h d f H1) (H0 h d f H1)))
(lift h d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 h d)))
k)))))))))) t).
(weight_map f (lift h d t1)) (weight_map f t1) (H h d f H1) (H0 h d f H1)))
(lift h d (THead (Flat f0) t0 t1)) (lift_head (Flat f0) t0 t1 h d)))
k)))))))))) t).
\lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(lift_weight_map t h d
(\lambda (_: nat).O) (\lambda (m: nat).(\lambda (_: (le d m)).(refl_equal nat
O)))))).
\lambda (t: T).(\lambda (h: nat).(\lambda (d: nat).(lift_weight_map t h d
(\lambda (_: nat).O) (\lambda (m: nat).(\lambda (_: (le d m)).(refl_equal nat
O)))))).
(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)).
(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)).
nat).(\lambda (H: (lt m O)).(lt_x_O m H (eq nat (wadd f w m) (f m)))))
(plus_n_O (wadd f w O)) (\lambda (m: nat).(\lambda (_: (le O m)).(refl_equal
nat (f m)))))))).
nat).(\lambda (H: (lt m O)).(lt_x_O m H (eq nat (wadd f w m) (f m)))))
(plus_n_O (wadd f w O)) (\lambda (m: nat).(\lambda (_: (le O m)).(refl_equal
nat (f m)))))))).
(d: nat).(eq_ind nat (weight (lift h d t)) (\lambda (n: nat).(lt n (weight
(THead k u (lift h d t))))) (tlt_head_dx k u (lift h d t)) (weight t)
(lift_weight t h d)))))).
(d: nat).(eq_ind nat (weight (lift h d t)) (\lambda (n: nat).(lt n (weight
(THead k u (lift h d t))))) (tlt_head_dx k u (lift h d t)) (weight t)
(lift_weight t h d)))))).