fact: Definition kfinite_subtype (X : UU) : UU := ∑ (A : hsubtype X), iskfinite (carrier A).
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.StandardFiniteSets UniMath.MoreFoundations.Subtypes UniMath.Combinatorics.KFiniteTypes