Lemma extend_tuple_dep_const {T A : UU} {n : nat} {f : stn n → T} {last : T} (af : stn n → A) (al : A) : extend_tuple_dep (T := T) (A := λ _, A) (f := f) (last := last) af al = extend_tuple af al. Proof. apply funextsec. intro i. unfold extend_tuple, extend_tuple_dep. now induction (invweq (weqdnicoprod _ lastelement) i). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.