Proofgold Term Root Disambiguation

∀ x0 . CRing_with_id 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
b501f..^{CRing_with_id_omega_exp_S}

theory
HotG

stx
339e9..

address
TMaPK..^{CRing_with_id_omega_exp_S}