∀ (motive : EReal → Sort u_1) (h_1 : Unit → motive none) (h_2 : Unit → motive (some none))
  (h_3 : (x : ℝ) → motive (some (some x))),
  (match some none with
    | none => h_1 ()
    | some none => h_2 ()
    | some (some x) => h_3 x) =
    h_2 ()