∀ {Γ : Type u_1} [inst : Inhabited Γ] {Λ : Type u_2} [inst_1 : Inhabited Λ] (M : Turing.TM0.Machine Γ Λ),
  StateTransition.Respects (Turing.TM0.step M) (Turing.TM1.step (Turing.TM0to1.tr M)) fun a b =>
    Turing.TM0to1.trCfg M a = b