{α : Type u_2} →
  {β : Type u_1} →
    {r : α → α → Prop} →
      {s : β → β → Prop} →
        (motive : PrincipalSeg r s ⊕ (r ≃r s) → Sort u_3) →
          (x : PrincipalSeg r s ⊕ (r ≃r s)) →
            ((f' : PrincipalSeg r s) → motive (Sum.inl f')) → ((f' : r ≃r s) → motive (Sum.inr f')) → motive x