Lemma tl_vec_map {A B : UU} (f : A → B) {n} (v : vec A (S n)) : tl (vec_map f v) = vec_map f (tl v). Proof. reflexivity. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.