Definition stnweq {n : nat} : stn n ⨿ unit ≃ stn (1 + n) := weqdnicoprod _ lastelement.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.