You have to define the way that the sort should work though, and at that point, what you really want is functional dependencies. Coq, Idris, Agda, etc, etc. No

You have to define the way that the sort should work though, and at that point, what you really want is functional dependencies. Coq, Idris, Agda, etc, etc. Not a lot of fun to learn how they work, but they're really quite impressive.