Proofgold Term Root Disambiguation

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

as obj
00081..^{struct_p_nonempty}

as prop
-

theory
HotG

stx
2c45b..

address
TMPfq..^{struct_p_nonempty}