Definition subtype_from_finite_subset {X : hSet} (A : finite_subset X) : hsubtype X := pr1 A.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.