Proofgold Term Root Disambiguation

λ x0 . ap x0 5

as obj
e9023..^{RealsStruct_one}

as prop
-

theory
HotG

stx
8f02a..

address
TMG8f..^{RealsStruct_one}