proposition: Lemma weqstnsum1_eq' {n : nat} (f : ⟦n⟧ -> nat) : invmap (weqstnsum1 f) = weqstnsum_invmap f.
proof: Proof. intros. apply idpath. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions