Proofgold Term Root Disambiguation

λ x0 x1 x2 . unpack_e_o x0 (λ x3 x4 . unpack_e_o x1 (λ x5 x6 . and (x2 ∈ setexp x5 x3) (ap x2 x4 = x6)))

as obj
0f504..^Hom_struct_e

as prop
-

theory
HotG

stx
820be..

address
TMQMK..^Hom_struct_e