Lemma iskfinite_union {I X : UU} (index : I → hsubtype X) (Ifinite : isfinite I) (index_finite : ∏ (i : I), iskfinite (index i)) : iskfinite (⋃ index). Proof. assert(finitechoicebase : ∥ ∏ (i : I), kfinstruct (index i) ∥). { use ischoicebasefiniteset. apply Ifinite. apply index_finite. } use(hinhfun2 _ Ifinite finitechoicebase). intro; apply kfinstruct_union. now apply kfinstruct_finstruct. Qed.
Require Import UniMath.Foundations.Propositions. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.Combinatorics.FiniteSets. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.Combinatorics.KFiniteTypes.