\forall (e: C).(\forall (hds: PList).(\forall (c: C).((drop1 hds c e) \to
(\forall (ts: TList).((sns3 e ts) \to (sns3 c (lifts1 hds ts)))))))
\def
\forall (e: C).(\forall (hds: PList).(\forall (c: C).((drop1 hds c e) \to
(\forall (ts: TList).((sns3 e ts) \to (sns3 c (lifts1 hds ts)))))))
\def