Proofgold Term Root Disambiguation

∀ x0 . RealsStruct x0 ⟶ ∀ x1 : ο . ((∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ Field_minus (Field_of_RealsStruct x0) x2 ∈ RealsStruct_Z x0) ⟶ field4 x0 ∈ RealsStruct_Z x0 ⟶ RealsStruct_Npos x0 ⊆ RealsStruct_Z x0 ⟶ RealsStruct_Z x0 ⊆ field0 x0 ⟶ (∀ x2 . x2 ∈ RealsStruct_Z x0 ⟶ ∀ x3 : ο . (Field_minus (Field_of_RealsStruct x0) x2 ∈ RealsStruct_Npos x0 ⟶ x3) ⟶ (x2 = field4 x0 ⟶ x3) ⟶ (x2 ∈ RealsStruct_Npos x0 ⟶ x3) ⟶ x3) ⟶ RealsStruct_one x0 ∈ RealsStruct_Z x0 ⟶ Field_minus (Field_of_RealsStruct x0) (RealsStruct_one x0) ∈ RealsStruct_Z x0 ⟶ (∀ x2 . x2 ∈ RealsStruct_Z x0 ⟶ Field_minus (Field_of_RealsStruct x0) x2 ∈ RealsStruct_Z x0) ⟶ (∀ x2 . x2 ∈ RealsStruct_Z x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Z x0 ⟶ field1b x0 x2 x3 ∈ RealsStruct_Z x0) ⟶ (∀ x2 . x2 ∈ RealsStruct_Z x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Z x0 ⟶ field2b x0 x2 x3 ∈ RealsStruct_Z x0) ⟶ x1) ⟶ x1

as obj
-

as prop
5f0a7..^{RealsStruct_Z_props}

theory
HotG

stx
56719..

address
TMSzN..^{RealsStruct_Z_props}