proposition: 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: Proof. apply funextsec. intro i. unfold extend_tuple, extend_tuple_dep. now induction (invweq (weqdnicoprod _ lastelement) i). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors