Definition finite_singleton {X : hSet} (x : X) : finite_subset X. Proof. use make_finite_subset. - exact(singleton x). - exact isfinite_singleton. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.