{α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → (α → Option β) → Sort u_3) →
      (x : Option α) →
        (x_1 : α → Option β) →
          ((x : α → Option β) → motive none x) → ((a : α) → (f : α → Option β) → motive (some a) f) → motive x x_1