Definition finstructondecsubset {X : UU} (f : X -> bool) (sx : finstruct X) : finstruct (hfiber f true) := make_finstruct _ (weqcomp (invweq (pr2 (weqfromdecsubsetofstn (f ∘ sx)))) (weqhfibersgwtog _ f true)).
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.