∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (x : List Bool) (x_1 : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ),
  Turing.TM1to1.write x x_1 =
    match x, x_1 with
    | [], q => q
    | a :: l, q =>
      Turing.TM1.Stmt.write (fun x x_2 => a) (Turing.TM1.Stmt.move Turing.Dir.right (Turing.TM1to1.write l q))