Proofgold Term Root Disambiguation

λ x0 x1 x2 . and (and (subfield x0 x1) (x2 ∈ setminus (field0 x1) (field0 x0))) (∀ x3 . subfield x0 x3 ⟶ x2 ∈ field0 x3 ⟶ subfield x1 x3)

as obj
937ed..^{Field_extension_by_1}

as prop
-

theory
HotG

stx
6b5ba..

address
TMQQt..^{Field_extension_by_1}