Definition isfinitetotal2 {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). use(hinhfun2 _ fs' sx). intros. apply finstructontotal2; assumption. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions. Require Import UniMath.MoreFoundations.Subtypes.