∀ {R : Type u} [inst : CommSemiring R] (p q p' q' : Polynomial R) (hpq : p.comp q = Polynomial.X)
  (hqp : q.comp p = Polynomial.X) (hpq' : p'.comp q' = Polynomial.X) (hqp' : q'.comp p' = Polynomial.X),
  (p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp') = (p = p')