\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((sty1 g c
t1 t2) \to (\forall (v1: T).(\forall (v2: T).((sty0 g c v1 v2) \to (ex2 T
(\lambda (v3: T).(sty1 g c v1 v3)) (\lambda (v3: T).(sty1 g c (THead (Flat
\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t2: T).((sty1 g c
t1 t2) \to (\forall (v1: T).(\forall (v2: T).((sty0 g c v1 v2) \to (ex2 T
(\lambda (v3: T).(sty1 g c v1 v3)) (\lambda (v3: T).(sty1 g c (THead (Flat