\forall (k: K).(\forall (c1: C).(\forall (x: C).(\forall (u1: T).(\forall
(v: T).(\forall (i: nat).((csubst1 (s k i) v (CHead c1 k u1) x) \to (ex3_2 T
C (\lambda (u2: T).(\lambda (c2: C).(eq C x (CHead c2 k u2)))) (\lambda (u2:
\forall (k: K).(\forall (c1: C).(\forall (x: C).(\forall (u1: T).(\forall
(v: T).(\forall (i: nat).((csubst1 (s k i) v (CHead c1 k u1) x) \to (ex3_2 T
C (\lambda (u2: T).(\lambda (c2: C).(eq C x (CHead c2 k u2)))) (\lambda (u2: