Proofgold Term Root Disambiguation

λ x0 . decode_b (ap x0 1)

as obj
ed06a..^{RealsStruct_plus}

as prop
-

theory
HotG

stx
8f02a..

address
TMYTM..^{RealsStruct_plus}