\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h:
nat).(\forall (d: nat).((ty3 g c (lift h d t1) x) \to (\forall (e: C).((drop
h d c e) \to (ex2 T (\lambda (t2: T).(pc3 c (lift h d t2) x)) (\lambda (t2:
\forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h:
nat).(\forall (d: nat).((ty3 g c (lift h d t1) x) \to (\forall (e: C).((drop
h d c e) \to (ex2 T (\lambda (t2: T).(pc3 c (lift h d t2) x)) (\lambda (t2: