DEFINITION bind_dec_not()
TYPE =
       ∀b1:B.∀b2:B.(or (eq B b1 b2) (not (eq B b1 b2)))
BODY =
Show proof