proposition: Fact vec_list_vec_set_pos n f : vec_list (@vec_set_pos n f) = map f (pos_list n).
proof: Proof. revert f; induction n as [ | n IHn ]; intros f; simpl; f_equal; auto. rewrite IHn, map_map; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)