Proofgold Term Root Disambiguation

λ x0 . {x1 ∈ RealsStruct_N x0|x1 = field4 x0 ⟶ ∀ x2 : ο . x2}

as obj
f5d38..^{RealsStruct_Npos}

as prop
-

theory
HotG

stx
56719..

address
TMXGA..^{RealsStruct_Npos}