Definition isfiniteforall {X : UU} (P : X -> UU) (sx : isfinite X) (fs : ∏ x : X , isfinite (P x)) : isfinite (∏ (x : X) , P x). Proof. set (fs' := ischoicebasefiniteset sx _ fs). exact(hinhfun2 (fun a b => finstructonforall P b a) fs' sx). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.