proposition: 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: Proof. apply vec_extens. intro i. rewrite el_vec_map. rewrite el_make_vec. rewrite el_make_vec. apply idpath. Defined.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers