∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ)
  {k : K} (o : Turing.TM2to1.StAct K Γ σ k) (q : Turing.TM2.Stmt Γ Λ σ) (v : σ) {S : List (Γ k)}
  {L : Turing.ListBlank ((k : K) → Option (Γ k))},
  Turing.ListBlank.map (Turing.proj k) L = Turing.ListBlank.mk (List.map some S).reverse →
    ∀ n ≤ S.length,
      StateTransition.Reaches₀ (Turing.TM1.step (Turing.TM2to1.tr M))
        { l := some (Turing.TM2to1.Λ'.go k o q), var := v, Tape := Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L) }
        { l := some (Turing.TM2to1.Λ'.go k o q), var := v,
          Tape := (Turing.Tape.move Turing.Dir.right)^[n] (Turing.Tape.mk' ∅ (Turing.TM2to1.addBottom L)) }