{α : Type u_2} →
  {β : Type u_1} →
    (motive : β ⊕ α → Sort u_3) →
      (x : β ⊕ α) →
        ((b : β) → x = Sum.inl b → motive (Sum.inl b)) → ((a' : α) → x = Sum.inr a' → motive (Sum.inr a')) → motive x