Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . pack_e x0 x2 = pack_e x1 x3 ⟶ and (x0 = x1) (x2 = x3)

as obj
-

as prop
0e751..^pack_e_inj

theory
HotG

stx
3fdf8..

address
TMbTR..^pack_e_inj