fact: 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)).
imports: UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions UniMath.Combinatorics.StandardFiniteSets UniMath.MoreFoundations.Subtypes