chore: revert reducibility change `PartialOrder.rel`

This PR is similar to #12403.

We previously conjectured that "all type class fields that are types
should be marked as reducible." The problem is that propositions are
types, but they are also used as data (with `Decidable`).
For example, we often see the proposition `x <= y` as a Boolean.
So, we refined the conjecture to:

"All type class fields that are types (and not propositions) should be marked as reducible."