proposition: Fact vec_change_eq n v p q x : p = q -> vec_pos (@vec_change n v p x) q = x.
proof: Proof. intro; subst q; revert p x. induction v; intros p ?; invert pos p; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)