DEFINITION csubv_bind_same()
TYPE =
       ∀c1:C
         .∀c2:C
           .csubv c1 c2
             →∀b:B.∀v1:T.∀v2:T.(csubv (CHead c1 (Bind b) v1) (CHead c2 (Bind b) v2))
BODY =
Show proof