Definition subsetFiniteSet {X : FiniteSet} (P : DecidableSubtype X) : FiniteSet. Proof. exact(isfinite_to_FiniteSet (subsetFiniteness (pr2 X) P)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.