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