-(n: nat).(le (f n) (g n)))) \to (le (weight_map f t0) (weight_map g t0))))))
-\to (\forall (t1: T).(((\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)))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
-\to nat))).(((\forall (n: nat).(le (f n) (g n)))) \to (le (match b0 with
-[Abbr \Rightarrow (S (plus (weight_map f t0) (weight_map (wadd f (S
-(weight_map f t0))) t1))) | Abst \Rightarrow (S (plus (weight_map f t0)
-(weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus (weight_map f t0)
-(weight_map (wadd f O) t1)))]) (match b0 with [Abbr \Rightarrow (S (plus
-(weight_map g t0) (weight_map (wadd g (S (weight_map g t0))) t1))) | Abst
-\Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O) t1))) | Void
-\Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O)
+(n: nat).(le (f n) (g n)))) \to (le (weight_map f t1) (weight_map g t1))))))
+\to (\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
+(n: nat).(le (f n) (g n)))) \to (le (weight_map f (THead k0 t0 t1))
+(weight_map g (THead k0 t0 t1))))))))))) (\lambda (b: B).(B_ind (\lambda (b0:
+B).(\forall (t0: T).(((\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)))))) \to (\forall (t1: T).(((\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)))))) \to (\forall (f: ((nat \to
+nat))).(\forall (g: ((nat \to nat))).(((\forall (n: nat).(le (f n) (g n))))
+\to (le (match b0 with [Abbr \Rightarrow (S (plus (weight_map f t0)
+(weight_map (wadd f (S (weight_map f t0))) t1))) | Abst \Rightarrow (S (plus
+(weight_map f t0) (weight_map (wadd f O) t1))) | Void \Rightarrow (S (plus
+(weight_map f t0) (weight_map (wadd f O) t1)))]) (match b0 with [Abbr
+\Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g (S (weight_map g
+t0))) t1))) | Abst \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g
+O) t1))) | Void \Rightarrow (S (plus (weight_map g t0) (weight_map (wadd g O)