Commit 2022-08-17 04:40 08931580
View on Github →refactor(order/rel_classes): redefine is_well_order
in terms of is_well_founded
(#15729)
We redefine is_well_order
in terms of is_well_founded
, and remove the redundant is_irrefl
assumption in the process.
This also replaces is_well_order.wf
with is_well_founded.wf
.