∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (x : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stmts₁ x =
    match x with
    | Q@h:(Turing.TM2.Stmt.push k a q) => insert Q (Turing.TM2.stmts₁ q)
    | Q@h:(Turing.TM2.Stmt.peek k a q) => insert Q (Turing.TM2.stmts₁ q)
    | Q@h:(Turing.TM2.Stmt.pop k a q) => insert Q (Turing.TM2.stmts₁ q)
    | Q@h:(Turing.TM2.Stmt.load a q) => insert Q (Turing.TM2.stmts₁ q)
    | Q@h:(Turing.TM2.Stmt.branch a q₁ q₂) => insert Q (Turing.TM2.stmts₁ q₁ ∪ Turing.TM2.stmts₁ q₂)
    | Q@h:(Turing.TM2.Stmt.goto a) => {Q}
    | Q@h:Turing.TM2.Stmt.halt => {Q}