Proofgold Term Root Disambiguation

λ x0 . ∀ x1 : ι → ο . (∀ x2 x3 . x3 ∈ x2 ⟶ x1 (pack_e x2 x3)) ⟶ x1 x0

as obj
59de6..^struct_e

as prop
-

theory
HotG

stx
3fdf8..

address
TMJWW..^struct_e