proposition: Lemma transport_stnsum {m n : nat} (e: m=n) (g: ⟦n⟧ -> nat) : stnsum g = stnsum (λ i, g(transportf stn e i)).
proof: Proof. intros. induction e. apply idpath. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.DecidablePropositions UniMath.MoreFoundations.NegativePropositions