Proofgold Term Root Disambiguation

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

as obj
2a63f..

as prop
-

theory
HotG

stx
56719..

address
TMMed..