proposition: Fact vec_map_map X Y Z (f : X -> Y) (g : Y -> Z) n (v : vec _ n) : vec_map g (vec_map f v) = vec_map (fun x => g (f x)) v.
proof: Proof. induction v; simpl; f_equal; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)