nat).(\lambda (H0: (le v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
nat).(le (wadd f v n0) (wadd g w n0))) H0 (\lambda (n0: nat).(\lambda (_: (le
(wadd f v n0) (wadd g w n0))).(H n0))) n))))))).
nat).(\lambda (H0: (le v w)).(\lambda (n: nat).(nat_ind (\lambda (n0:
nat).(le (wadd f v n0) (wadd g w n0))) H0 (\lambda (n0: nat).(\lambda (_: (le
(wadd f v n0) (wadd g w n0))).(H n0))) n))))))).
nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S (S v) w H0))
(\lambda (n0: nat).(\lambda (_: (le (wadd f v n0) (wadd g w n0))).(H n0)))
n))))))).
nat).(le (wadd f v n0) (wadd g w n0))) (le_S_n v w (le_S (S v) w H0))
(\lambda (n0: nat).(\lambda (_: (le (wadd f v n0) (wadd g w n0))).(H n0)))
n))))))).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (wadd (\lambda (_:
nat).O) O n0) O)) (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat
(wadd (\lambda (_: nat).O) O n0) O)).(refl_equal nat O))) n).
\lambda (n: nat).(nat_ind (\lambda (n0: nat).(eq nat (wadd (\lambda (_:
nat).O) O n0) O)) (refl_equal nat O) (\lambda (n0: nat).(\lambda (_: (eq nat
(wadd (\lambda (_: nat).O) O n0) O)).(refl_equal nat O))) n).
(weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g
t1)) (le_plus_plus (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1)
(weight_map g t1) (H f0 g H1) (H0 f0 g H1))))))))))) k)) t).
(weight_map f0 t0) (weight_map f0 t1)) (plus (weight_map g t0) (weight_map g
t1)) (le_plus_plus (weight_map f0 t0) (weight_map g t0) (weight_map f0 t1)
(weight_map g t1) (H f0 g H1) (H0 f0 g H1))))))))))) k)) t).
nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n)
(H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0:
nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))).
nat).(eq_ind_r nat (g n) (\lambda (n0: nat).(le n0 (g n))) (le_n (g n)) (f n)
(H n)))) (weight_le t g f (\lambda (n: nat).(eq_ind_r nat (g n) (\lambda (n0:
nat).(le (g n) n0)) (le_n (g n)) (f n) (H n)))))))).
\def
\lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_:
nat).O) (\lambda (n: nat).(wadd_O n))).
\def
\lambda (t: T).(weight_eq t (wadd (\lambda (_: nat).O) O) (\lambda (_:
nat).O) (\lambda (n: nat).(wadd_O n))).
(wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(wadd_le (\lambda (_:
nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_n O)) O (S m) (le_S O m
(le_O_n m)) n)))).
(wadd (\lambda (_: nat).O) (S m)) (\lambda (n: nat).(wadd_le (\lambda (_:
nat).O) (\lambda (_: nat).O) (\lambda (_: nat).(le_n O)) O (S m) (le_S O m
(le_O_n m)) n)))).
\lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u)
(weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u)
(weight v) (weight t) H H0))))).
\lambda (v: T).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (lt (weight u)
(weight v))).(\lambda (H0: (lt (weight v) (weight t))).(lt_trans (weight u)
(weight v) (weight t) H H0))))).
(weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u)
(weight_map (\lambda (_: nat).O) t)) (le_plus_l (weight_map (\lambda (_:
nat).O) u) (weight_map (\lambda (_: nat).O) t)))))) k).
(weight_map (\lambda (_: nat).O) u) (plus (weight_map (\lambda (_: nat).O) u)
(weight_map (\lambda (_: nat).O) t)) (le_plus_l (weight_map (\lambda (_:
nat).O) u) (weight_map (\lambda (_: nat).O) t)))))) k).
(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))
(le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
nat).O) t)))))) k).
(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t))
(le_plus_r (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_:
nat).O) t)))))) k).
Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t)
n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight
t)))))).
Prop))).(\lambda (H: ((\forall (n: nat).(\forall (t: T).((eq nat (weight t)
n) \to (P t)))))).(\lambda (t: T).(H (weight t) t (refl_equal nat (weight
t)))))).
t1)))))) H0 (weight t0) H1) in (H t0 (\lambda (v: T).(\lambda (H3: (lt
(weight v) (weight t0))).(H2 (weight v) H3 v (refl_equal nat (weight
v))))))))))))) t)))).
t1)))))) H0 (weight t0) H1) in (H t0 (\lambda (v: T).(\lambda (H3: (lt
(weight v) (weight t0))).(H2 (weight v) H3 v (refl_equal nat (weight
v))))))))))))) t)))).