fact: Definition make_finite_subset {X : hSet} (A : hsubtype X) (P : isfinite (carrier A)) : finite_subset X := (A ,, P).
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions UniMath.Combinatorics.StandardFiniteSets UniMath.MoreFoundations.Subtypes