proposition: Fact vec_list_vec_map (f : X -> Y) n v : vec_list (@vec_map X Y f n v) = map f (vec_list 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)