Proofgold Term Root Disambiguation

∀ x0 . RealsStruct x0 ⟶ ∀ x1 . x1 ∈ setexp (field0 x0) (RealsStruct_N x0) ⟶ ∀ x2 . x2 ∈ setexp (field0 x0) (RealsStruct_N x0) ⟶ (∀ x3 . x3 ∈ RealsStruct_N x0 ⟶ and (and (RealsStruct_leq x0 (ap x1 x3) (ap x2 x3)) (RealsStruct_leq x0 (ap x1 x3) (ap x1 (field1b x0 x3 (RealsStruct_one x0))))) (RealsStruct_leq x0 (ap x2 (field1b x0 x3 (RealsStruct_one x0))) (ap x2 x3))) ⟶ ∃ x3 . and (x3 ∈ field0 x0) (∀ x5 . x5 ∈ RealsStruct_N x0 ⟶ and (RealsStruct_leq x0 (ap x1 x5) x3) (RealsStruct_leq x0 x3 (ap x2 x5)))

as obj
-

as prop
bf523..^{RealsStruct_Compl}

theory
HotG

stx
8f02a..

address
TMSCe..^{RealsStruct_Compl}