Proofgold Term Root Disambiguation

∃ x0 : ι → ι → ο . and (stricttotalorder x0) (∀ x2 : ι → ο . (∃ x3 . x2 x3) ⟶ ∃ x3 . and (x2 x3) (∀ x5 . and (x2 x5) (x5 = x3 ⟶ ∀ x6 : ο . x6) ⟶ x0 x3 x5))

as obj
-

as prop
f5c42..

theory
HoTg

stx
75b72..

address
TMGPa..^{Zermelo_WO_strict}