proposition: Fact vec_change_same n v p : @vec_change n v p (vec_pos v p) = v.
proof: Proof. apply vec_pos_ext; intros q. destruct (pos_eq_dec p q). + repeat rewrite vec_change_eq; subst; auto. + repeat rewrite vec_change_neq; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)