Proofgold Term Root Disambiguation

λ x0 x1 x2 . ∀ x3 : ο . (∀ x4 . and (x4 ∈ RealsStruct_Npos x0) (field2b x0 x1 x4 = x2) ⟶ x3) ⟶ x3

as obj
26b0f..^{RealsStruct_divides}

as prop
-

theory
HotG

stx
0f4f5..

address
TMSgv..^{RealsStruct_divides}