proposition: Lemma vec_change_same' {X : Type} {n : nat} {v : vec X n} {p : pos n} {x : X} : vec_pos v p = x -> vec_change v p x = v.
proof: Proof. move=> <-. by apply: vec_change_same. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun