DEFINITION terms_props__bind_dec()
TYPE =
       ∀b1:B.∀b2:B.(or (eq B b1 b2) (eq B b1 b2)→∀P:Prop.P)
BODY =
Show proof