proposition: Lemma vec_map_comp {A B C: UU} (f: A → B) (g: B → C) {n: nat} (v: vec A n) : vec_map (funcomp f g) v = (funcomp (vec_map f) (vec_map g)) v.
proof: Proof. revert n v. refine (vec_ind _ _ _). - apply idpath. - intros x n xs HPxs. apply vecS_eq. + reflexivity. + apply HPxs. Defined.
imports: UniMath.Combinatorics.StandardFiniteSets UniMath.Foundations.NaturalNumbers