I've implemented functional induction theorems in Lean, shipping with the upcoming version 4.8.0, and wrote a tutorial-style blog post about it: https://lean-lang.org/blog/2024-5-17-functional-induction/
(h't to David Christiansen for the tooling behind the hover features.) #lean#leanlang
