DEFINITION bind_dec_not()
TYPE =
       ∀b1:B.∀b2:B.(or (eq B b1 b2) (not (eq B b1 b2)))
BODY =
        assume b1: B
        assume b2: B
          (H_x) 
             by (terms_props__bind_dec . .)
or (eq B b1 b2) (eq B b1 b2)→∀P:Prop.P
          end of H_x
          (H) consider H_x
          we proceed by induction on H to prove or (eq B b1 b2) (eq B b1 b2)→False
             case or_introl : H0:eq B b1 b2 ⇒
                the thesis becomes or (eq B b1 b2) (eq B b1 b2)→False
                   by (or_introl . . H0)
or (eq B b1 b2) (eq B b1 b2)→False
             case or_intror : H0:(eq B b1 b2)→∀P:Prop.P ⇒
                the thesis becomes or (eq B b1 b2) (eq B b1 b2)→False
                   suppose H1: eq B b1 b2
                      by (H0 H1 .)
                      we proved False
                   we proved (eq B b1 b2)→False
                   by (or_intror . . previous)
or (eq B b1 b2) (eq B b1 b2)→False
          we proved or (eq B b1 b2) (eq B b1 b2)→False
          that is equivalent to or (eq B b1 b2) (not (eq B b1 b2))
       we proved ∀b1:B.∀b2:B.(or (eq B b1 b2) (not (eq B b1 b2)))