Ordering package:parameterized-utils

Ordering over two distinct types with a proof they are equal.
Convert standard ordering to OrderingF.
joinOrderingF x y first compares on x, returning an equivalent value if it is not EQF. If it is EQF, it returns y.
Convert OrderingF to standard ordering.