Proofgold Term Root Disambiguation

λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . λ x6 . ∃ x7 . and (x7 ∈ {x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9 ∈ {x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1 ⟶ ∀ x11 : ο . x11}) (x9 = x1)) (x9 ∈ {x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1 ⟶ ∀ x11 : ο . x11})}) (∃ x9 . and (x9 ∈ {x11 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x11 = x1 ⟶ ∀ x12 : ο . x12}) (x4 x9 x6 = x7))

as obj
6449a..^{explicit_OrderedField_rationalp}

as prop
-

theory
HotG

stx
b2e5e..

address
TMS9J..^{explicit_OrderedField_rationalp}