\forall (g: G).(\forall (c2: C).(\forall (e2: C).(\forall (d: nat).(\forall
(h: nat).((drop h d c2 e2) \to (\forall (e1: C).((csubc g e2 e1) \to (ex2 C
(\lambda (c1: C).(drop h d c1 e1)) (\lambda (c1: C).(csubc g c2 c1))))))))))
\forall (g: G).(\forall (c2: C).(\forall (e2: C).(\forall (d: nat).(\forall
(h: nat).((drop h d c2 e2) \to (\forall (e1: C).((csubc g e2 e1) \to (ex2 C
(\lambda (c1: C).(drop h d c1 e1)) (\lambda (c1: C).(csubc g c2 c1))))))))))