\forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (i:
nat).((getl i c (CHead e (Bind b) u)) \to (flt e u c (TLRef i)))))))
\def
\forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (i:
nat).((getl i c (CHead e (Bind b) u)) \to (flt e u c (TLRef i)))))))
\def