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