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