Commit 2025-01-10 17:21 59439d6b
View on Github →feat: Make PNat.recOn induction eliminator (#20617)
Following this discussion on Zulip:
https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Base.20Case.20for.20Induction.20on.20N.2B/near/492807806