j))))) (\lambda (u3: T).(\lambda (c2: C).(\lambda (_: nat).(eq C c0 (CHead c2
k u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
u3)))) (\lambda (_: T).(\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1
j))))) (\lambda (u3: T).(\lambda (c2: C).(\lambda (_: nat).(eq C c0 (CHead c2
k u3))))) (\lambda (u3: T).(\lambda (_: C).(\lambda (j: nat).(subst0 j v u1
u3)))) (\lambda (_: T).(\lambda (c2: C).(\lambda (j: nat).(csubst0 j v c1