{α : Type u_1} →
  (motive : Option α → Option α → Sort u_2) →
    (x x_1 : Option α) →
      (Unit → motive none none) →
        ((a b : α) → motive (some a) (some b)) → ((x x_2 : Option α) → motive x x_2) → motive x x_1