∀ {Γ : Type u_1} (motive : Turing.TM0.Stmt Γ → Sort u_2) (a : Γ)
  (h_1 : (d : Turing.Dir) → motive (Turing.TM0.Stmt.move d)) (h_2 : (a : Γ) → motive (Turing.TM0.Stmt.write a)),
  (match Turing.TM0.Stmt.write a with
    | Turing.TM0.Stmt.move d => h_1 d
    | Turing.TM0.Stmt.write a => h_2 a) =
    h_2 a