proposition: 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: Proof. reflexivity. Defined.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers