fact: Definition kfinstruct_stn_indexed {n : nat} (P : ⟦ n ⟧ → UU) (index : ∏ (k : ⟦ n ⟧), kfinstruct (P k)) : kfinstruct (∑ (k : ⟦ n ⟧), P k).
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Notations UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.StandardFiniteSets