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