Commit 2022-07-20 16:22 1dd65b6a
View on Github →refactor(order/rel_classes): ditch is_extensional (#15373)
This typeclass was barely used anyways, and the instances that existed for it had unnecessary assumptions. We replace it by the theorem extensional_of_trichotomous_of_irrefl.
A relevant short discussion on this typeclass: link