\forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (d:
nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
(m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to
\forall (w: nat).(\forall (t: T).(\forall (h: nat).(\forall (d:
nat).(\forall (f: ((nat \to nat))).(\forall (g: ((nat \to nat))).(((\forall
(m: nat).((lt m d) \to (eq nat (g m) (f m))))) \to ((eq nat (g d) w) \to