\forall (b: B).(\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i:
nat).((getl i c (CHead d (Bind b) u)) \to (\forall (k: K).(\forall (v:
T).(getl i (CTail k v c) (CHead (CTail k v d) (Bind b) u)))))))))
\forall (b: B).(\forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i:
nat).((getl i c (CHead d (Bind b) u)) \to (\forall (k: K).(\forall (v:
T).(getl i (CTail k v c) (CHead (CTail k v d) (Bind b) u)))))))))