proposition: Fact vec_map_set_pos X Y f n s : @vec_map X Y f _ (@vec_set_pos _ n s) = vec_set_pos (fun p => f (s p)).
proof: Proof. apply vec_pos_ext; intros p. rewrite vec_pos_map, vec_pos_set, vec_pos_set; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)