∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥) (g : Polynomial K),
  ↑((RatFunc.Luroth.algEquiv h) ((algebraMap (Polynomial K) (RatFunc K)) g)) =
    (Polynomial.aeval (RatFunc.Luroth.generator E)) g