proposition: Lemma vec_app_eq {T : Type} {n m} {v : Vector.t T n} {w : Vector.t T m} : Vector.append v w = vec_app v w.
proof: Proof. elim: v. { by rewrite vec_app_nil. } move=> > /= ->. by rewrite vec_app_cons. Qed.
imports: Undecidability(TM.TM) Undecidability.MinskyMachines(MM MMA MMA.mma_defs Util.MMA_computable) Undecidability.Shared.Libs.DLW(Vec.pos Vec.vec Code.sss) List PeanoNat Lia Relations ssreflect