proposition: 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: Proof. unfold extend_tuple. refine (maponpaths _ (_ : invmap stnweq i = inr tt)). apply (invmaponpathsweq (weqdnicoprod n lastelement)). refine (homotweqinvweq _ _ @ _). apply stn_eq. apply Hi. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors