fact: Definition kfinite_subtype_property {X} (A : kfinite_subtype X) : iskfinite (carrier A) := pr2 A.
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.StandardFiniteSets UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.KFiniteTypes