C).(\lambda (H0: (csubst1 i v c1 c2)).(eq_ind nat (s (Flat f) i) (\lambda (n:
nat).(csubst1 n v (CHead c1 (Flat f) u1) (CHead c2 (Flat f) u2)))
(csubst1_head (Flat f) i v u1 u2 H c1 c2 H0) i (refl_equal nat i)))))))))).
C).(\lambda (H0: (csubst1 i v c1 c2)).(eq_ind nat (s (Flat f) i) (\lambda (n:
nat).(csubst1 n v (CHead c1 (Flat f) u1) (CHead c2 (Flat f) u2)))
(csubst1_head (Flat f) i v u1 u2 H c1 c2 H0) i (refl_equal nat i)))))))))).