Lemma extend_tuple_i {T : UU} {n : nat} (f : stn n → T) (last : T) (i : nat) (Hi1 : i < S n) (Hi2 : i < n) : extend_tuple f last (i ,, Hi1) = f (make_stn _ i Hi2). Proof. unfold extend_tuple. refine (maponpaths _ (_ : invmap stnweq (i ,, Hi1) = inl (make_stn _ i Hi2))). apply (invmaponpathsweq (weqdnicoprod n lastelement)). refine (homotweqinvweq _ _ @ _). apply stn_eq. refine (!di_eq1 _). apply Hi2. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.