(v: T).(\lambda (H: (csubst0 i v c1 c2)).(\lambda (u: T).(eq_ind nat (s (Bind
b) i) (\lambda (n: nat).(csubst0 n v (CHead c1 (Bind b) u) (CHead c2 (Bind b)
u))) (csubst0_fst (Bind b) i c1 c2 v H u) (S i) (refl_equal nat (S i))))))))).
(v: T).(\lambda (H: (csubst0 i v c1 c2)).(\lambda (u: T).(eq_ind nat (s (Bind
b) i) (\lambda (n: nat).(csubst0 n v (CHead c1 (Bind b) u) (CHead c2 (Bind b)
u))) (csubst0_fst (Bind b) i c1 c2 v H u) (S i) (refl_equal nat (S i))))))))).