Proofgold Term Root Disambiguation

∀ x0 . RealsStruct x0 ⟶ ∀ x1 : ο . (RealsStruct_Npos x0 ⊆ field0 x0 ⟶ explicit_Nats (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x2 . field1b x0 x2 (RealsStruct_one x0)) ⟶ RealsStruct_one x0 ∈ RealsStruct_Npos x0 ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ field1b x0 x2 (RealsStruct_one x0) = RealsStruct_one x0 ⟶ ∀ x3 : ο . x3) ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ ∀ x3 : ι → ο . x3 (RealsStruct_one x0) ⟶ (∀ x4 . x4 ∈ RealsStruct_Npos x0 ⟶ x3 (field1b x0 x4 (RealsStruct_one x0))) ⟶ x3 x2) ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Npos x0 ⟶ explicit_Nats_one_plus (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x5 . field1b x0 x5 (RealsStruct_one x0)) x2 x3 = field1b x0 x2 x3) ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Npos x0 ⟶ explicit_Nats_one_mult (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x5 . field1b x0 x5 (RealsStruct_one x0)) x2 x3 = field2b x0 x2 x3) ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Npos x0 ⟶ field1b x0 x2 x3 ∈ RealsStruct_Npos x0) ⟶ (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x2 x3 ∈ RealsStruct_Npos x0) ⟶ x1) ⟶ x1

as obj
-

as prop
a2de5..^{RealsStruct_Npos_props}

theory
HotG

stx
56719..

address
TMUvj..^{RealsStruct_Npos_props}