∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → Sort u_4)
  (h_1 : (a : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.move a q))
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.write a q))
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.load a q))
  (h_4 : (a : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → motive (Turing.TM1.Stmt.branch a q₁ q₂))
  (h_5 : (l : Γ → σ → Λ) → motive (Turing.TM1.Stmt.goto l)) (h_6 : Unit → motive Turing.TM1.Stmt.halt),
  (match Turing.TM1.Stmt.halt with
    | Turing.TM1.Stmt.move a q => h_1 a q
    | Turing.TM1.Stmt.write a q => h_2 a q
    | Turing.TM1.Stmt.load a q => h_3 a q
    | Turing.TM1.Stmt.branch a q₁ q₂ => h_4 a q₁ q₂
    | Turing.TM1.Stmt.goto l => h_5 l
    | Turing.TM1.Stmt.halt => h_6 ()) =
    h_6 ()