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