Lemma extend_tuple_eq {T : UU} {n : nat} {last : T} {f : stn n → T} {g : stn (S n) → T} (Hf : ∏ i, f i = g (stnweq (inl i))) (Hlast : last = g (stnweq (inr tt))) : extend_tuple f last = g. Proof. apply funextfun. intro i. unfold extend_tuple. refine (_ @ maponpaths g (homotweqinvweq stnweq i)). induction (invmap stnweq i) as [i' | i']. - exact (Hf i'). - exact Hlast. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.