\forall (c1: C).(\forall (c2: C).((cimp c1 c2) \to (\forall (b: B).(\forall
(d1: C).(\forall (w: T).(\forall (i: nat).((getl i c1 (CHead d1 (Bind b) w))
\to (ex2 C (\lambda (d2: C).(cimp d1 d2)) (\lambda (d2: C).(getl i c2 (CHead
\forall (c1: C).(\forall (c2: C).((cimp c1 c2) \to (\forall (b: B).(\forall
(d1: C).(\forall (w: T).(\forall (i: nat).((getl i c1 (CHead d1 (Bind b) w))
\to (ex2 C (\lambda (d2: C).(cimp d1 d2)) (\lambda (d2: C).(getl i c2 (CHead