\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c
(CHead d (Bind Abbr) u)) \to ((nf2 c (TLRef i)) \to (\forall (P: Prop).P))))))
\def
\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c
(CHead d (Bind Abbr) u)) \to ((nf2 c (TLRef i)) \to (\forall (P: Prop).P))))))
\def