{α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          ((val : β) → motive none (some val)) →
            ((x : α) → (y : β) → motive (some x) (some y)) →
              ((x : Option α) →
                  (x_2 : Option β) →
                    (∀ (val : β), x = none → x_2 = some val → False) →
                      (∀ (x_4 : α) (y : β), x = some x_4 → x_2 = some y → False) → motive x x_2) →
                motive x x_1