Lemma extend_tuple_last {T : UU} {n : nat} (f : stn n → T) (last : T) (i : stn (S n)) (Hi : stntonat _ i = n) : extend_tuple f last i = last. Proof. unfold extend_tuple. refine (maponpaths _ (_ : invmap stnweq i = inr tt)). apply (invmaponpathsweq (weqdnicoprod n lastelement)). refine (homotweqinvweq _ _ @ _). apply stn_eq. apply Hi. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.