fact: Definition subtype_from_finite_subset {X : hSet} (A : finite_subset X) : hsubtype X := pr1 A.
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions UniMath.Combinatorics.StandardFiniteSets UniMath.MoreFoundations.Subtypes