∀ {α : Type u_1} {β : Type u_2} (motive : Option α → Option β → Sort u_3) (val : β)
  (h_1 : (val : β) → motive none (some val)) (h_2 : Unit → motive none none) (h_3 : (val : α) → motive (some val) none)
  (h_4 : (x : α) → (y : β) → motive (some x) (some y)),
  (match none, some val with
    | none, some val => h_1 val
    | none, none => h_2 ()
    | some val, none => h_3 val
    | some x, some y => h_4 x y) =
    h_1 val