fact: Definition left := fun (t : tape) => match t with | niltape => [] | leftof _ _ => [] | rightof s l => s :: l | midtape l _ _ => l end.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM