Proofgold Term Root Disambiguation

λ x0 . {x1 ∈ field0 x0|or (or (Field_minus (Field_of_RealsStruct x0) x1 ∈ RealsStruct_Npos x0) (x1 = field4 x0)) (x1 ∈ RealsStruct_Npos x0)}

as obj
0610d..^{RealsStruct_Z}

as prop
-

theory
HotG

stx
56719..

address
TMZnq..^{RealsStruct_Z}