Commit 2021-07-10 18:38 8b4628e4
View on Github →feat(data/fintype/basic): induction principle for finite types (#8158)
This lets us prove things about finite types by induction, analogously to proving things about natural numbers by induction. Here pempty plays the role of 0 and option plays the role of nat.succ. We need an extra hypothesis that our statement is invariant under equivalence of types. Used in #8019.