Proofgold Term Root Disambiguation

∀ x0 x1 x2 . 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) ⟶ Field_automorphism_fixing x0 x1 x2

as obj
-

as prop
b9288..^{Field_automorphism_fixing_I}

theory
HotG

stx
6b5ba..

address
TMSoh..^{Field_automorphism_fixing_I}