Proofgold Term Root Disambiguation

∀ x0 . CRing_with_id x0 ⟶ x0 = pack_b_b_e_e (field0 x0) (field1b x0) (field2b x0) (field3 x0) (field4 x0)

as obj
-

as prop
d44bb..^CRing_eta

theory
HotG

stx
339e9..

address
TMGYe..^CRing_eta