Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 . PtdSetHom (pack_e x0 x2) (pack_e x1 x3) x4 = and (x4 ∈ setexp x1 x0) (ap x4 x2 = x3)

as obj
-

as prop
f65a3..^{Hom_struct_e_pack}

theory
HotG

stx
820be..

address
TMH3g..^{Hom_struct_e_pack}