Proofgold Term Root Disambiguation

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

as obj
816f6..^{radical_field_extension}

as prop
-

theory
HotG

stx
6b5ba..

address
TMchE..^{radical_field_extension}