Definition finite_singleton_is_in {X : hSet} (A : hsubtype X) (a : A) : finite_singleton (pr1 a) ⊆ A. Proof. apply singleton_is_in. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.