\forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c
(CHead d (Bind Abbr) w)) \to (\forall (vs: TList).((sn3 c (THeads (Flat Appl)
vs (lift (S i) O w))) \to (sn3 c (THeads (Flat Appl) vs (TLRef i)))))))))
\forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c
(CHead d (Bind Abbr) w)) \to (\forall (vs: TList).((sn3 c (THeads (Flat Appl)
vs (lift (S i) O w))) \to (sn3 c (THeads (Flat Appl) vs (TLRef i)))))))))