∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trNormal (Turing.TM2.Stmt.push k a q) =
    Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.push a) q