Definition isfinite_to_FiniteSet {X : UU} (f : isfinite X) : FiniteSet := X ,, f.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.