Proofgold Term Root Disambiguation

λ x0 . decode_r (ap x0 3)

as obj
e6607..^{RealsStruct_leq}

as prop
-

theory
HotG

stx
8f02a..

address
TMVpP..^{RealsStruct_leq}