nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
(weight_map f t0) (weight_map (wadd f (S (weight_map f t0))) t1)) (plus
(weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1))
-(plus_le_compat (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S
+(le_plus_plus (weight_map f t0) (weight_map g t0) (weight_map (wadd f (S
(weight_map f t0))) t1) (weight_map (wadd g (S (weight_map g t0))) t1) (H f g
H1) (H0 (wadd f (S (weight_map f t0))) (wadd g (S (weight_map g t0)))
(\lambda (n: nat).(wadd_le f g H1 (S (weight_map f t0)) (S (weight_map g t0))
(g n)))) \to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat
\to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le
(f n) (g n))))).(le_n_S (plus (weight_map f t0) (weight_map (wadd f O) t1))
-(plus (weight_map g t0) (weight_map (wadd g O) t1)) (plus_le_compat
-(weight_map f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map
-(wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n:
-nat).(wadd_le f g H1 O O (le_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H:
-((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (n:
-nat).(le (f n) (g n)))) \to (le (weight_map f t0) (weight_map g
-t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f: ((nat \to
+(plus (weight_map g t0) (weight_map (wadd g O) t1)) (le_plus_plus (weight_map
+f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map (wadd g O) t1)
+(H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O
+(le_n O) n)))))))))))) (\lambda (t0: T).(\lambda (H: ((\forall (f: ((nat \to
nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
-\to (le (weight_map f t1) (weight_map g t1))))))).(\lambda (f: ((nat \to
-nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le (f
-n) (g n))))).(le_n_S (plus (weight_map f t0) (weight_map (wadd f O) t1))
-(plus (weight_map g t0) (weight_map (wadd g O) t1)) (plus_le_compat
-(weight_map f t0) (weight_map g t0) (weight_map (wadd f O) t1) (weight_map
-(wadd g O) t1) (H f g H1) (H0 (wadd f O) (wadd g O) (\lambda (n:
-nat).(wadd_le f g H1 O O (le_n O) n)))))))))))) b)) (\lambda (_: F).(\lambda
-(t0: T).(\lambda (H: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
-nat))).(((\forall (n: nat).(le (f0 n) (g n)))) \to (le (weight_map f0 t0)
-(weight_map g t0))))))).(\lambda (t1: T).(\lambda (H0: ((\forall (f0: ((nat
-\to nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g
-n)))) \to (le (weight_map f0 t1) (weight_map g t1))))))).(\lambda (f0: ((nat
-\to nat))).(\lambda (g: ((nat \to nat))).(\lambda (H1: ((\forall (n: nat).(le
-(f0 n) (g n))))).(le_n_S (plus (weight_map f0 t0) (weight_map f0 t1)) (plus
-(weight_map g t0) (weight_map g t1)) (plus_le_compat (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).
+\to (le (weight_map f t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
+(H0: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
+(n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g
+t1))))))).(\lambda (f: ((nat \to nat))).(\lambda (g: ((nat \to
+nat))).(\lambda (H1: ((\forall (n: nat).(le (f n) (g n))))).(le_n_S (plus
+(weight_map f t0) (weight_map (wadd f O) t1)) (plus (weight_map g t0)
+(weight_map (wadd g O) t1)) (le_plus_plus (weight_map f t0) (weight_map g t0)
+(weight_map (wadd f O) t1) (weight_map (wadd g O) t1) (H f g H1) (H0 (wadd f
+O) (wadd g O) (\lambda (n: nat).(wadd_le f g H1 O O (le_n O) n))))))))))))
+b)) (\lambda (_: F).(\lambda (t0: T).(\lambda (H: ((\forall (f0: ((nat \to
+nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f0 n) (g n))))
+\to (le (weight_map f0 t0) (weight_map g t0))))))).(\lambda (t1: T).(\lambda
+(H0: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
+(n: nat).(le (f0 n) (g n)))) \to (le (weight_map f0 t1) (weight_map g
+t1))))))).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to
+nat))).(\lambda (H1: ((\forall (n: nat).(le (f0 n) (g n))))).(le_n_S (plus
+(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).
theorem weight_eq:
\forall (t: T).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to