proposition: Lemma vec_change_swap [X] [n] (v : vec X n) (p : pos n) (q : pos n) x y : p <> q -> v[x / p][y / q] = v [y / q][x / p].
proof: Proof. intros Hnew. eapply vec_pos_ext. intros r. destruct (pos_eq_dec q r). - subst. rewrite vec_change_eq, vec_change_neq, vec_change_eq; congruence. - destruct (pos_eq_dec p r). + subst. rewrite vec_change_neq, vec_change_eq, vec_change_eq; congruence. + rewrite !vec_change_neq; congruence. Qed.
imports: Undecidability.MinskyMachines(MM_computable MM_sss mm_utils) Undecidability.StackMachines(BSM_computable) Undecidability.Shared.Libs.DLW(vec pos sss subcode) Lia Vector Nat Arith List Undecidability.MinskyMachines.MM(mm_defs mm_utils mm_comp_strong)