∀ {α : Type u_1} (motive : WithBot α → WithBot α → Sort u_2) (a : α) (h_1 : (x : WithBot α) → motive x none)
  (h_2 : (a : α) → motive none (some a)) (h_3 : (a b : α) → motive (some a) (some b)),
  (match none, some a with
    | x, none => h_1 x
    | none, some a => h_2 a
    | some a, some b => h_3 a b) =
    h_2 a