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 LambdaCalculus.Krivine LambdaCalculus.Util.Krivine_facts) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) PeanoNat List Lia ssreflect ssrbool ssrfun