You mean that, for instance, a standard-library generic sort function, might require that your comparator function behave correctly when the arguments are rever

You mean that, for instance, a standard-library generic sort function, might require that your comparator function behave correctly when the arguments are reversed? That's an interesting idea. Like Java interfaces, but with formal contracts. I doubt that putting these contracts into the standard-library would give you good proof-coverage though.