{α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          ((a : α) → (b : β) → motive (some a) (some b)) →
            ((x : Option α) →
                (x_2 : Option β) → (∀ (a : α) (b : β), x = some a → x_2 = some b → False) → motive x x_2) →
              motive x x_1