{R : Type u} →
  {S : Type v} →
    {inst : CommSemiring R} →
      {inst_1 : Semiring S} →
        {inst_2 : Algebra R S} →
          {f : Polynomial R} →
            {P : Sort u_1} →
              {toIsAdjoinRoot : IsAdjoinRoot S f} →
                {monic : f.Monic} →
                  {toIsAdjoinRoot' : IsAdjoinRoot S f} →
                    {monic' : f.Monic} →
                      { toIsAdjoinRoot := toIsAdjoinRoot, monic := monic } =
                          { toIsAdjoinRoot := toIsAdjoinRoot', monic := monic' } →
                        (toIsAdjoinRoot ≍ toIsAdjoinRoot' → P) → P