Proofgold Term Root Disambiguation

∀ x0 x1 . subfield x0 x1 ⟶ ∀ x2 : ο . (Field x0 ⟶ Field x1 ⟶ field0 x0 ⊆ field0 x1 ⟶ field3 x0 = field3 x1 ⟶ field4 x0 = field4 x1 ⟶ (∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ field1b x0 x3 x4 = field1b x1 x3 x4) ⟶ (∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ field2b x0 x3 x4 = field2b x1 x3 x4) ⟶ x2) ⟶ x2

as obj
-

as prop
e75e5..^subfield_E

theory
HotG

stx
6b5ba..

address
TMTNH..^subfield_E