\forall (i: nat).(\forall (d: nat).((lt i d) \to (\forall (c1: C).(\forall
(c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (b: B).(\forall (e2:
C).(\forall (v: T).((getl i c2 (CHead e2 (Bind b) v)) \to (ex2 C (\lambda
\forall (i: nat).(\forall (d: nat).((lt i d) \to (\forall (c1: C).(\forall
(c2: C).(\forall (h: nat).((drop h d c1 c2) \to (\forall (b: B).(\forall (e2:
C).(\forall (v: T).((getl i c2 (CHead e2 (Bind b) v)) \to (ex2 C (\lambda