\forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
u t z) \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
\forall (u: T).(\forall (t: T).(\forall (z: T).(\forall (d: nat).((subst0 d
u t z) \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