\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i
O c1 (CHead d1 (Bind Abbr) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba
g c2 c1) \to (or3 (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abbr)
\forall (i: nat).(\forall (c1: C).(\forall (d1: C).(\forall (u1: T).((drop i
O c1 (CHead d1 (Bind Abbr) u1)) \to (\forall (g: G).(\forall (c2: C).((csuba
g c2 c1) \to (or3 (ex2 C (\lambda (d2: C).(drop i O c2 (CHead d2 (Bind Abbr)