Definition flatten' {X:UU} {n:nat} {m: ⟦n⟧ -> nat} : (∏ (i: ⟦n⟧ ), ⟦m i⟧ -> X) -> ( ⟦stnsum m⟧ -> X). Proof. intros g. exact (uncurry g ∘ invmap (weqstnsum1 m)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.