\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
(n: nat).((getl n c1 (CHead d1 (Bind Abbr) u)) \to (\forall (c2: C).((csubt g
c1 c2) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n
\forall (g: G).(\forall (c1: C).(\forall (d1: C).(\forall (u: T).(\forall
(n: nat).((getl n c1 (CHead d1 (Bind Abbr) u)) \to (\forall (c2: C).((csubt g
c1 c2) \to (ex2 C (\lambda (d2: C).(csubt g d1 d2)) (\lambda (d2: C).(getl n