Proofgold Term Root Disambiguation

λ x0 . decode_b (ap x0 2)

as obj
7eb39..^{RealsStruct_mult}

as prop
-

theory
HotG

stx
8f02a..

address
TMQST..^{RealsStruct_mult}