proposition: Lemma stnsum_1 (n : nat) : stnsum(λ i: ⟦n⟧, 1) = n.
proof: Proof. intros. induction n as [|n IH]. { apply idpath. } simpl. use (natpluscomm _ _ @ _). apply maponpaths. exact IH. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions