Proofgold Term Root Disambiguation

∀ x0 . CRing_with_id x0 ⟶ field4 x0 ∈ field0 x0

as obj
-

as prop
a5370..^{CRing_with_id_one_In}

theory
HotG

stx
339e9..

address
TMSn9..^{CRing_with_id_one_In}