Proofgold Term Root Disambiguation

λ x0 . binunion x0 (Sing x0)

as obj
1452f..^ordsucc

as prop
-

theory
HotG

stx
18c18..

address
TMavR..^ordsucc