We should be able to use constraint ordering on ordinals.

Open craff opened this issue 3 years ago • 0 comments

This is needed to write subtyping proof manually (and checking termination giving exact induction hyp). Need a use case first ?

Jul 27 '22 01:07 craff