Commit 2024-05-11 18:18 f851598b
View on Github →refactor: nicer well-founded function definitions (#12628)
by preferring decreasing_by over inline proofs, the resulting
equational theorems are nicer.
Also we can use functional induction in one case rather nicely.