Proofgold Term Root Disambiguation

λ x0 . Sep (field0 x0) (natOfOrderedField_p (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_leq x0))

as obj
49868..^{RealsStruct_N}

as prop
-

theory
HotG

stx
8f02a..

address
TMbcM..^{RealsStruct_N}