∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) (k : K)
  (f : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (f : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k f q))
  (h_2 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k f q))
  (h_3 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k f q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (x : Turing.TM2.Stmt Γ Λ σ) → motive x),
  (match Turing.TM2.Stmt.push k f q with
    | Turing.TM2.Stmt.push k f q => h_1 k f q
    | Turing.TM2.Stmt.peek k f q => h_2 k f q
    | Turing.TM2.Stmt.pop k f q => h_3 k f q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | x => h_6 x) =
    h_1 k f q