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