Definition lexicalEnumeration {n : nat} (m: ⟦n⟧ -> nat) : ⟦stnsum m⟧ ≃ (∑ i : ⟦n⟧, ⟦m i⟧) := invweq (weqstnsum1 m).
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.