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. intros. exact (nat_plus_associativity (uncurry k)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.