Proofgold Term Root Disambiguation

λ x0 x1 x2 . and (and (and (subfield x1 x0) (Field_Hom x0 x0 x2)) (∀ x3 . x3 ∈ ap x0 0 ⟶ ∃ x4 . and (x4 ∈ ap x0 0) (ap x2 x4 = x3))) (∀ x3 . x3 ∈ ap x1 0 ⟶ ap x2 x3 = x3)

as obj
8e98c..^{Field_automorphism_fixing}

as prop
-

theory
HotG

stx
6b5ba..

address
TMN78..^{Field_automorphism_fixing}