u3)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v0 c1
c3)))) u2 c2 i0 (refl_equal nat (s k i0)) (refl_equal C (CHead c2 k u2)) H12
H11)) k0 H8))))))) H6)) H5))))))))))))) i v y x H0))) H))))))).
u3)))) (\lambda (_: T).(\lambda (c3: C).(\lambda (j: nat).(csubst0 j v0 c1
c3)))) u2 c2 i0 (refl_equal nat (s k i0)) (refl_equal C (CHead c2 k u2)) H12
H11)) k0 H8))))))) H6)) H5))))))))))))) i v y x H0))) H))))))).