Definition finstructonforall {X : UU} (P : X -> UU) (sx : finstruct X) (fs : ∏ x : X , finstruct (P x)) : finstruct (∏ x : X , P x) := make_finstruct _ (nelstructonforall P _ sx fs).
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.