Proofgold Term Root Disambiguation

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

as obj
e29a2..^struct_u_bij

as prop
-

theory
HotG

stx
7469b..

address
TMcDM..^struct_u_bij