Commit 2024-09-17 10:56 f18da2b2
View on Github →feat(Order/InitialSeg): Subsingleton (α ≃o β) on well-orders (#16882)
This allows us to generalize an instance which stated this for Fin n.
We also generalize StrictMono.range_inj for maps into preorders.