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