-t2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
-nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
-i) O v)) (g i)) \to (le (weight_map f t2) (weight_map g t1)))))))).(\lambda
-(u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat \to nat))).(\lambda
-(H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda (H3: (lt (weight_map f0
-(lift (S i) O v)) (g i))).(lt_le_S (plus (weight_map f0 u0) (weight_map f0
-t2)) (S (plus (weight_map g u0) (weight_map g t1))) (le_lt_n_Sm (plus
-(weight_map f0 u0) (weight_map f0 t2)) (plus (weight_map g u0) (weight_map g
-t1)) (plus_le_compat (weight_map f0 u0) (weight_map g u0) (weight_map f0 t2)
-(weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2 H3)))))))))))))))) k))
-(\lambda (v: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda (i: nat).(\lambda
-(_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall (f: ((nat \to nat))).(\forall
-(g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt
-(weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f u2) (weight_map
-g u1)))))))).(\lambda (k: K).(K_ind (\lambda (k0: K).(\forall (t1:
-T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to (((\forall (f: ((nat \to
-nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
-\to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s k0 i))) \to (le
-(weight_map f t2) (weight_map g t1))))))) \to (\forall (f: ((nat \to
-nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m) (g m))))
-\to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map f (THead
-k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b: B).(B_ind
-(\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s (Bind b0) i) v
-t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to
-nat))).(((\forall (m: nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S
-(s (Bind b0) i)) O v)) (g (s (Bind b0) i))) \to (le (weight_map f t2)
-(weight_map g t1))))))) \to (\forall (f: ((nat \to nat))).(\forall (g: ((nat
+t2)).(\lambda (H1: ((\forall (f0: ((nat \to nat))).(\forall (g: ((nat \to
+nat))).(((\forall (m: nat).(le (f0 m) (g m)))) \to ((lt (weight_map f0 (lift
+(S i) O v)) (g i)) \to (le (weight_map f0 t2) (weight_map g
+t1)))))))).(\lambda (u0: T).(\lambda (f0: ((nat \to nat))).(\lambda (g: ((nat
+\to nat))).(\lambda (H2: ((\forall (m: nat).(le (f0 m) (g m))))).(\lambda
+(H3: (lt (weight_map f0 (lift (S i) O v)) (g i))).(lt_le_S (plus (weight_map
+f0 u0) (weight_map f0 t2)) (S (plus (weight_map g u0) (weight_map g t1)))
+(le_lt_n_Sm (plus (weight_map f0 u0) (weight_map f0 t2)) (plus (weight_map g
+u0) (weight_map g t1)) (plus_le_compat (weight_map f0 u0) (weight_map g u0)
+(weight_map f0 t2) (weight_map g t1) (weight_le u0 f0 g H2) (H1 f0 g H2
+H3)))))))))))))))) k)) (\lambda (v: T).(\lambda (u1: T).(\lambda (u2:
+T).(\lambda (i: nat).(\lambda (_: (subst0 i v u1 u2)).(\lambda (H1: ((\forall
+(f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f
+m) (g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le
+(weight_map f u2) (weight_map g u1)))))))).(\lambda (k: K).(K_ind (\lambda
+(k0: K).(\forall (t1: T).(\forall (t2: T).((subst0 (s k0 i) v t1 t2) \to
+(((\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m:
+nat).(le (f m) (g m)))) \to ((lt (weight_map f (lift (S (s k0 i)) O v)) (g (s
+k0 i))) \to (le (weight_map f t2) (weight_map g t1))))))) \to (\forall (f:
+((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall (m: nat).(le (f m)
+(g m)))) \to ((lt (weight_map f (lift (S i) O v)) (g i)) \to (le (weight_map
+f (THead k0 u2 t2)) (weight_map g (THead k0 u1 t1)))))))))))) (\lambda (b:
+B).(B_ind (\lambda (b0: B).(\forall (t1: T).(\forall (t2: T).((subst0 (s
+(Bind b0) i) v t1 t2) \to (((\forall (f: ((nat \to nat))).(\forall (g: ((nat