Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ο . struct_p (pack_p x0 x1)

as obj
-

as prop
d2435..^{pack_struct_p_I}

theory
HotG

stx
3fdf8..

address
TMUKc..^{pack_struct_p_I}