proposition: Lemma extend_tuple_eq {T : UU} {n : nat} {last : T} {f : stn n → T} {g : stn (S n) → T} (Hf : ∏ i, f i = g (stnweq (inl i))) (Hlast : last = g (stnweq (inr tt))) : extend_tuple f last = g.
proof: Proof. apply funextfun. intro i. unfold extend_tuple. refine (_ @ maponpaths g (homotweqinvweq stnweq i)). induction (invmap stnweq i) as [i' | i']. - exact (Hf i'). - exact Hlast. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors