Definition subsetFiniteness {X : UU} (is : isfinite X) (P : DecidableSubtype X) : isfinite (decidableSubtypeCarrier P). Proof. intros. assert (fin : isfinite (decidableSubtypeCarrier' P)). { now apply isfinitedecsubset. } refine (isfiniteweqf _ fin). apply decidableSubtypeCarrier_weq. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.