DEFINITION csubst0_snd_bind()
TYPE =
       ∀b:B
         .∀i:nat
           .∀v:T
             .∀u1:T
               .∀u2:T
                 .(subst0 i v u1 u2)→∀c:C.(csubst0 (S i) v (CHead c (Bind b) u1) (CHead c (Bind b) u2))
BODY =
Show proof