Proofgold Term Root Disambiguation

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

as obj
-

as prop
9308b..^Field_eta

theory
HotG

stx
339e9..

address
TMcWS..^Field_eta