Proofgold Term Root Disambiguation

∀ x0 . Field x0 ⟶ ∀ x1 x2 . x2 ∈ omega ⟶ CRing_with_id_omega_exp x0 x1 (ordsucc x2) = field2b x0 x1 (CRing_with_id_omega_exp x0 x1 x2)

as obj
-

as prop
41463..^{Field_omega_exp_S}

theory
HotG

stx
339e9..

address
TMRxJ..^{Field_omega_exp_S}