∀ {β : Type u_1} (motive : Option β → Sort u_2) (x : Option β) (h_1 : Unit → motive none)
  (h_2 : (b : β) → motive (some b)),
  x = none →
    (match x with
      | none => h_1 ()
      | some b => h_2 b) ≍
      h_1 ()