{Γ : Type u_1} →
  {Λ : Type u_2} →
    (motive : Option (Λ × Turing.TM0.Stmt Γ) → Sort u_3) →
      (x : Option (Λ × Turing.TM0.Stmt Γ)) →
        (Unit → motive none) → ((q' : Λ) → (s : Turing.TM0.Stmt Γ) → motive (some (q', s))) → motive x