proposition: Lemma vec_pos_cons {T : Type} {n} {w : Vector.t T n} x X : vec_pos (x ## w) (Fin.FS X) = vec_pos w X.
proof: Proof. done. Qed.
imports: Undecidability(MinskyMachines.MM MinskyMachines.MMA L.L) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss Code.subcode) Undecidability(MinskyMachines.Util.MMA_pairing L.AbstractMachines.wCBV) PeanoNat List Lia Wf_nat ssreflect ssrbool ssrfun