Proofgold Term Root Disambiguation

∀ x0 . RealsStruct x0 ⟶ ∀ x1 : ο . (RealsStruct_Q x0 ⊆ field0 x0 ⟶ (∀ x2 . x2 ∈ RealsStruct_Q x0 ⟶ ∀ x3 : ο . (x2 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ RealsStruct_Z x0 ⟶ ∀ x5 . x5 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x5 x2 = x4 ⟶ x3) ⟶ x3) ⟶ (∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Z x0 ⟶ ∀ x4 . x4 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x4 x2 = x3 ⟶ x2 ∈ RealsStruct_Q x0) ⟶ x1) ⟶ x1

as obj
-

as prop
61a49..^{RealsStruct_Q_props}

theory
HotG

stx
56719..

address
TMHAB..^{RealsStruct_Q_props}