Proofgold Term Root Disambiguation

λ x0 . and (struct_p x0) (unpack_p_o x0 (λ x1 . λ x2 : ι → ο . ∃ x3 . and (x3 ∈ x1) (x2 x3)))

as obj
00081..^{struct_p_nonempty}

as prop
-

theory
HotG

stx
2c45b..

address
TMPfq..^{struct_p_nonempty}