{P : Sort u} →
  {α : Type u_5} →
    {β : Type u_6} →
      {inst : NonAssocSemiring α} →
        {inst_1 : NonAssocSemiring β} →
          {t : α →+* β} →
            {α' : Type u_5} →
              {β' : Type u_6} →
                {inst' : NonAssocSemiring α'} →
                  {inst'_1 : NonAssocSemiring β'} →
                    {t' : α' →+* β'} →
                      α = α' → β = β' → inst ≍ inst' → inst_1 ≍ inst'_1 → t ≍ t' → RingHom.noConfusionType P t t'