\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
(i: nat).((getl i c1 (CHead d1 (Bind Abst) u)) \to (\forall (c2: C).((csuba g
c2 c1) \to (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u)))
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
(i: nat).((getl i c1 (CHead d1 (Bind Abst) u)) \to (\forall (c2: C).((csuba g
c2 c1) \to (or (ex2 C (\lambda (d2: C).(getl i c2 (CHead d2 (Bind Abst) u)))