{P : Sort u} →
  {R : Type u_2} →
    {inst : Semiring R} →
      {t : RingInvo R} →
        {R' : Type u_2} →
          {inst' : Semiring R'} → {t' : RingInvo R'} → R = R' → inst ≍ inst' → t ≍ t' → RingInvo.noConfusionType P t t'