feat(data/fintype/basic): induction principle for finite types (#8158)
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.





leanprover-community/mathlib,leanprover-community/mathlib