∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (M : Λ → Turing.TM1.Stmt Γ Λ σ)
  (motive : Turing.TM1to0.Λ' M → Γ → Sort u_4) (snd : σ) (x : Γ) (h_1 : (snd : σ) → (x : Γ) → motive (none, snd) x)
  (h_2 : (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (s : Γ) → motive (some q, v) s),
  (match (none, snd), x with
    | (none, snd), x => h_1 snd x
    | (some q, v), s => h_2 q v s) =
    h_1 snd x