Proofgold Term Root Disambiguation

∀ x0 x1 . struct_e (pack_e x0 x1) ⟶ x1 ∈ x0

as obj
-

as prop
550a7..^{pack_struct_e_E1}

theory
HotG

stx
3fdf8..

address
TMHRM..^{pack_struct_e_E1}