DEFINITION cimp_bind()
TYPE =
       ∀c1:C
         .∀c2:C
           .cimp c1 c2
             →∀b:B.∀v:T.(cimp (CHead c1 (Bind b) v) (CHead c2 (Bind b) v))
BODY =
Show proof