\forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((sty0 g e
t1 t2) \to (\forall (c: C).(\forall (h: nat).(\forall (d: nat).((drop h d c
e) \to (sty0 g c (lift h d t1) (lift h d t2))))))))))
\forall (g: G).(\forall (e: C).(\forall (t1: T).(\forall (t2: T).((sty0 g e
t1 t2) \to (\forall (c: C).(\forall (h: nat).(\forall (d: nat).((drop h d c
e) \to (sty0 g c (lift h d t1) (lift h d t2))))))))))