Proofgold Term Root Disambiguation

λ x0 x1 x2 . and (RealsStruct_leq x0 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3)

as obj
1fb82..^{RealsStruct_lt}

as prop
-

theory
HotG

stx
0f4f5..

address
TMZU8..^{RealsStruct_lt}