Address inconsistent style of typeclass laws

[omelkonian]

The laws for Eq are defined by asserting that the == decision procedure actually Reflects the type of propositional equality ≡, while the laws for Ord do not use this reflection style and just enumerate all the expected properties in a style suffering from "boolean blindness".

We should be consistent on how we go about all these similar situations, and in particular think how we should inter-operate with the standard library. (e.g. given that Ord reflects a definition that is not built-in like equality, but could be imported from stdlib's Data.Nat (≤), etc.).