\forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u
t1) \to (\forall (t2: T).((sty0 g c u t2) \to (ty3 g c u t2)))))))
\def
\forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t1: T).((ty3 g c u
t1) \to (\forall (t2: T).((sty0 g c u t2) \to (ty3 g c u t2)))))))
\def