Show that the type of Ferrers diagrams of any finite type is π-finite

[fredrik-bakke]

The following is waiting to be formalized in univalent-combinatorics.ferrers-diagrams:

• The type of Ferrers diagrams of any finite type is π-finite