\forall (g: G).(\forall (c: C).(\forall (t1: T).(or (ex T (\lambda (t2:
T).(ty3 g c t1 t2))) (\forall (t2: T).((ty3 g c t1 t2) \to False)))))
\def
\forall (g: G).(\forall (c: C).(\forall (t1: T).(or (ex T (\lambda (t2:
T).(ty3 g c t1 t2))) (\forall (t2: T).((ty3 g c t1 t2) \to False)))))
\def