{R : Type u₀} →
  [inst : CommSemiring R] →
    {A : Type u₁} →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] →
          {B : Type u₂} →
            [inst_3 : Ring B] →
              [inst_4 : Algebra R B] →
                {motive : IsMoritaEquivalent R A B → Sort u} →
                  (t : IsMoritaEquivalent R A B) → ((cond : Nonempty (MoritaEquivalence R A B)) → motive ⋯) → motive t