Proofgold Term Root Disambiguation

λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . λ x6 . ∃ x7 x9 . and (and (natOfOrderedField_p x0 x1 x2 x3 x4 x5 x7) (natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9)) (x4 x9 x6 = x7)

as obj
c3146..

as prop
-

theory
HotG

stx
80e8e..

address
TMKqg..