\forall (g: G).(\forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (u:
T).((ty3 g c (THead (Bind Abst) v t) u) \to ((pc3 c u v) \to (\forall (P:
Prop).P)))))))
\forall (g: G).(\forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (u:
T).((ty3 g c (THead (Bind Abst) v t) u) \to ((pc3 c u v) \to (\forall (P:
Prop).P)))))))