-(f n) (g n))))).(le_S_n (S (plus (weight_map f t0) (weight_map (wadd f O)
-t1))) (S (plus (weight_map g t0) (weight_map (wadd g O) t1))) (le_n_S (S
-(plus (weight_map f t0) (weight_map (wadd f O) t1))) (S (plus (weight_map g
-t0) (weight_map (wadd g O) t1))) (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 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_S_n (S (plus (weight_map f t0) (weight_map (wadd f O)
-t1))) (S (plus (weight_map g t0) (weight_map (wadd g O) t1))) (le_n_S (S
-(plus (weight_map f t0) (weight_map (wadd f O) t1))) (S (plus (weight_map g
-t0) (weight_map (wadd g O) t1))) (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))))).(lt_le_S (plus (weight_map f0 t0) (weight_map f0
-t1)) (S (plus (weight_map g t0) (weight_map g t1))) (le_lt_n_Sm (plus
+(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)))))))))))) (\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 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