Proofgold Term Root Disambiguation

∀ x0 x1 x2 . x2 ∈ omega ⟶ ∀ x3 . ap x3 0 = x0 ⟶ ap x3 x2 = x1 ⟶ (∀ x4 . x4 ∈ ordsucc x2 ⟶ Field (ap x3 x4)) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ field0 (ap x3 (ordsucc x4))) (∀ x7 : ο . (∀ x8 . and (x8 ∈ omega) (and (CRing_with_id_omega_exp (ap x3 (ordsucc x4)) x6 x8 ∈ field0 (ap x3 x4)) (Field_extension_by_1 (ap x3 x4) (ap x3 (ordsucc x4)) x6)) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ radical_field_extension x0 x1

as obj
-

as prop
6bd73..^{radical_field_extension_I}

theory
HotG

stx
6b5ba..

address
TMaTm..^{radical_field_extension_I}