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