proposition: Fact vec_change_neq n v p q x : p <> q -> vec_pos (@vec_change n v p x) q = vec_pos v q.
proof: Proof. revert p q x. induction v as [ | n y v IH ]; intros p q x H; invert pos p; invert pos q; auto. + destruct H; auto. + apply IH; contradict H; subst; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)