Proofgold Term Root Disambiguation

λ x0 x1 x2 . ∃ x3 . and (x3 ∈ RealsStruct_Npos x0) (field2b x0 x1 x3 = x2)

as obj
26b0f..^{RealsStruct_divides}

as prop
-

theory
HotG

stx
0f4f5..

address
TMSgv..^{RealsStruct_divides}