{P : Sort u} →
  {R : Type u_1} →
    {inst : NonUnitalNonAssocRing R} →
      {t : TwoSidedIdeal R} →
        {R' : Type u_1} →
          {inst' : NonUnitalNonAssocRing R'} →
            {t' : TwoSidedIdeal R'} → R = R' → inst ≍ inst' → t ≍ t' → TwoSidedIdeal.noConfusionType P t t'