\forall (b: B).(\forall (e: C).(\forall (d: C).(\forall (v: T).(\forall (i:
nat).((getl i (CHead e (Bind b) v) d) \to (or (land (eq nat i O) (eq C d
(CHead e (Bind b) v))) (ex2 nat (\lambda (j: nat).(eq nat i (S j))) (\lambda
\forall (b: B).(\forall (e: C).(\forall (d: C).(\forall (v: T).(\forall (i:
nat).((getl i (CHead e (Bind b) v) d) \to (or (land (eq nat i O) (eq C d
(CHead e (Bind b) v))) (ex2 nat (\lambda (j: nat).(eq nat i (S j))) (\lambda