proposition: Fact map_pos_list_vec n f : map f (pos_list n) = vec_list (@vec_set_pos n f).
proof: Proof. rewrite vec_list_vec_set_pos; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)