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