Proofgold Term Root Disambiguation

∀ x0 x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ap (ap (ap (Field_of_RealsStruct x0) 2) x1) x2 = field2b x0 x1 x2

as obj
-

as prop
b9ac9..^{Field_of_RealsStruct_2}

theory
HotG

stx
8f02a..

address
TMQiq..^{Field_of_RealsStruct_2}