∀ (q : Turing.PartrecToTM2.Λ') (s : Option Turing.PartrecToTM2.Γ') (a b c d : List Turing.PartrecToTM2.Γ'),
  Turing.Reaches₁ (Turing.TM2.step Turing.PartrecToTM2.tr)
    { l := some q.copy, var := s, stk := Turing.PartrecToTM2.K'.elim a b c d }
    { l := some q, var := none, stk := Turing.PartrecToTM2.K'.elim (b.reverseAux a) [] c (b.reverseAux d) }