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