Definition extend_tuple_dep {n : nat} {T : UU} {A : T → UU} {f : stn n → T} {last : T} (af : ∏ i, A (f i)) (alast : A last) : ∏ (i : stn (S n)), A (extend_tuple f last i). Proof. intro i. unfold extend_tuple. induction (invmap stnweq i) as [i' | ]. - exact (af i'). - exact alast. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.