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