DEFINITION pr2_gen_cbind()
TYPE =
       ∀b:B
         .∀c:C
           .∀v:T
             .∀t1:T
               .∀t2:T
                 .pr2 (CHead c (Bind b) v) t1 t2
                   →pr2 c (THead (Bind b) v t1) (THead (Bind b) v t2)
BODY =
Show proof