Commit 2025-10-26 12:59 bf1dbb96
View on Github →chore(Order/Defs): golf min_def (#30924)
After this change, min_def has a proof term that indicates that it is an alias of LinearOrder.min_def. So the duplicate declaration linter will not report it.