-(weight_map (\lambda (_: nat).O) u) n)))) (le_S_n (S (weight_map (\lambda (_:
-nat).O) t)) (S (plus (weight_map (\lambda (_: nat).O) u) (weight_map (\lambda
-(_: nat).O) t))) (le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus
-(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)))
-(le_n_S (weight_map (\lambda (_: nat).O) t) (plus (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))))) (weight_map
-(wadd (\lambda (_: nat).O) O) t) (weight_add_O t)))) (\lambda (u: T).(\lambda
-(t: T).(eq_ind_r nat (weight_map (\lambda (_: nat).O) t) (\lambda (n:
-nat).(lt (weight_map (\lambda (_: nat).O) t) (S (plus (weight_map (\lambda
-(_: nat).O) u) n)))) (le_S_n (S (weight_map (\lambda (_: nat).O) t)) (S (plus
-(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)))
-(le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda
-(_: nat).O) u) (weight_map (\lambda (_: nat).O) t))) (le_n_S (weight_map
-(\lambda (_: nat).O) t) (plus (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))))) (weight_map (wadd (\lambda (_:
-nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u:
-T).(\lambda (t: T).(le_S_n (S (weight_map (\lambda (_: nat).O) t)) (S (plus
-(weight_map (\lambda (_: nat).O) u) (weight_map (\lambda (_: nat).O) t)))
-(le_n_S (S (weight_map (\lambda (_: nat).O) t)) (S (plus (weight_map (\lambda
-(_: nat).O) u) (weight_map (\lambda (_: nat).O) t))) (le_n_S (weight_map
-(\lambda (_: nat).O) t) (plus (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) n)))) (le_n_S (weight_map (\lambda (_:
+nat).O) t) (plus (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))) (weight_map (wadd (\lambda (_: nat).O) O) t)
+(weight_add_O t)))) (\lambda (u: T).(\lambda (t: T).(eq_ind_r nat (weight_map
+(\lambda (_: nat).O) t) (\lambda (n: nat).(lt (weight_map (\lambda (_:
+nat).O) t) (S (plus (weight_map (\lambda (_: nat).O) u) n)))) (le_n_S
+(weight_map (\lambda (_: nat).O) t) (plus (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))) (weight_map (wadd (\lambda
+(_: nat).O) O) t) (weight_add_O t)))) b)) (\lambda (_: F).(\lambda (u:
+T).(\lambda (t: T).(le_n_S (weight_map (\lambda (_: nat).O) t) (plus
+(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).