∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : σ → Option (Γ k) → σ)
  (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stmts₁ (Turing.TM2.Stmt.peek k a q) = insert (Turing.TM2.Stmt.peek k a q) (Turing.TM2.stmts₁ q)