Lemma vec_map_make_vec {A B: UU} {n: nat} (g: ⟦ n ⟧ → A) (f: A → B) : vec_map f (make_vec g) = make_vec (f ∘ g). Proof. apply vec_extens. intro i. rewrite el_vec_map. rewrite el_make_vec. rewrite el_make_vec. apply idpath. Defined.
Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Foundations.NaturalNumbers.