∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ) (s : Γ) (x : σ) (a : Γ → σ → Γ)
  (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to0.trAux M s (Turing.TM1.Stmt.write a q) x = ((some q, x), Turing.TM0.Stmt.write (a s x))