∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a : Γ → σ → Bool) (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.stmts₁ (Turing.TM1.Stmt.branch a q₁ q₂) =
    insert (Turing.TM1.Stmt.branch a q₁ q₂) (Turing.TM1.stmts₁ q₁ ∪ Turing.TM1.stmts₁ q₂)