{α : Type u_1} →
  {β : Type u_2} →
    (motive : (x : α ⊕ β) → x.isRight = true → Sort u_3) →
      (x : α ⊕ β) →
        (x_1 : x.isRight = true) → ((b : β) → (x : (Sum.inr b).isRight = true) → motive (Sum.inr b) x) → motive x x_1