\forall (k: K).(\forall (b: B).(\forall (u1: T).(\forall (u2: T).(\forall
(c2: C).(\forall (c1: C).(\forall (i: nat).((getl i (CTail k u1 c1) (CHead c2
(Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e)))
\forall (k: K).(\forall (b: B).(\forall (u1: T).(\forall (u2: T).(\forall
(c2: C).(\forall (c1: C).(\forall (i: nat).((getl i (CTail k u1 c1) (CHead c2
(Bind b) u2)) \to (or (ex2 C (\lambda (e: C).(eq C c2 (CTail k u1 e)))