proposition: Corollary nat_plus_associativity' n (m:stn n->nat) (k:∏ i, stn (m i) -> nat) : stnsum (λ i, stnsum (k i)) = stnsum (uncurry (Z := λ _,_) k ∘ lexicalEnumeration m).
proof: Proof. intros. exact (nat_plus_associativity (uncurry k)). Defined.
imports: UniMath.Combinatorics.Lists UniMath.Combinatorics.FiniteSequences UniMath.Algebra.RigsAndRings UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.Algebra.Groups UniMath.MoreFoundations.NegativePropositions UniMath.Combinatorics.FiniteSets UniMath.Foundations.NaturalNumbers