Proofgold Term Root Disambiguation

λ x0 . {x1 ∈ RealsStruct_N x0|and (RealsStruct_lt x0 (RealsStruct_one x0) x1) (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ RealsStruct_divides x0 x2 x1 ⟶ or (x2 = RealsStruct_one x0) (x2 = x1))}

as obj
4f229..^{RealsStruct_Primes}

as prop
-

theory
HotG

stx
0f4f5..

address
TMZiA..^{RealsStruct_Primes}