∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trNormal (Turing.TM2.Stmt.load a q) = Turing.TM1.Stmt.load (fun x => a) (Turing.TM2to1.trNormal q)