Proofgold Term Root Disambiguation

∀ x0 . struct_e x0 ⟶ x0 = pack_e (ap x0 0) (ap x0 1)

as obj
-

as prop
bdc4a..^struct_e_eta

theory
HotG

stx
3fdf8..

address
TMUMV..^struct_e_eta