Proofgold Term Root Disambiguation

λ x0 . and (struct_u x0) (unpack_u_o x0 (λ x1 . inj x1 x1))

as obj
c2d02..^struct_u_inj

as prop
-

theory
HotG

stx
cbaa5..

address
TMJJh..^struct_u_inj