That's an interesting idea about a built-in ordered opaque value type. You should bring it up at the next monthly TLA+ foundation community call on November 14th![0] It would be interesting to hear peoples' feedback on it.

[0] Details hidden in the google calendar link on this thread in the mailing list: https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ/m/YrORpIfS...