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