∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (d : Turing.Dir)
  (q : Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ) (v : σ) (T : Turing.Tape Bool),
  Turing.TM1.stepAux (Turing.TM1to1.move n d q) v T = Turing.TM1.stepAux q v ((Turing.Tape.move d)^[n] T)