Definition FiniteSet_to_hSet (X : FiniteSet) : hSet := make_hSet (pr1 X) (isfinite_isaset (pr1 X) (pr2 X)).
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.