fact: Definition iskfinite (X : UU) : UU := ∥ kfinstruct X ∥.
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.StandardFiniteSets