The following is waiting to be formalized in `univalent-combinatorics.ferrers-diagrams`: - [ ] The type of Ferrers diagrams of any finite type is π-finite