\forall (g: G).(\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i:
nat).((getl i c (CHead d (Bind Abbr) v)) \to (\forall (vs: TList).(\forall
(a: A).((arity g c (THeads (Flat Appl) vs (lift (S i) O v)) a) \to (arity g c
\forall (g: G).(\forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i:
nat).((getl i c (CHead d (Bind Abbr) v)) \to (\forall (vs: TList).(\forall
(a: A).((arity g c (THeads (Flat Appl) vs (lift (S i) O v)) a) \to (arity g c