Definition extend_tuple {T : UU} {n : nat} (f : stn n → T) (last : T) : stn (S n) → T. Proof. intro i. induction (invmap stnweq i) as [i' | ]. - exact (f i'). - exact last. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.