proposition: Lemma vec_change_append_L {T : Type} {n} {w : Vector.t T n} {m} {v : Vector.t T m} {X} {x} : vec_change (Vector.append w v) (Fin.L m X) x = Vector.append (vec_change w X x) v.
proof: Proof. elim: X w. - move=> ? w. by rewrite (Vector.eta w). - move=> > IH /= w. by rewrite (Vector.eta w) /= IH. 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