\forall (e: C).(\forall (hds: PList).(\forall (c: C).(\forall (t: T).((drop1
hds c e) \to ((nf2 e t) \to (nf2 c (lift1 hds t)))))))
\def
\forall (e: C).(\forall (hds: PList).(\forall (c: C).(\forall (t: T).((drop1
hds c e) \to ((nf2 e t) \to (nf2 c (lift1 hds t)))))))
\def