How does one write an induction principle?
As a frequent naturals-induction-principle user I was mindblown when I first discovered that one can use induction on other types and that one can in fact write an induction principle from scratch.
As a frequent naturals-induction-principle user I was mindblown when I first discovered that one can use induction on other types and that one can in fact write an induction principle from scratch.