proposition: Lemma vec_change_comm {X} n v p q x y : p <> q -> vec_change (@vec_change X n v p x) q y = vec_change (vec_change v q y) p x.
proof: Proof. intros Hpq. apply vec_pos_ext; intros r. destruct (pos_eq_dec r p); destruct (pos_eq_dec r q); subst; now rew vec. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)