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