Proofgold Term Root Disambiguation

λ x0 x1 . and (ZermeloWO x0 x1) (x0 = x1 ⟶ ∀ x2 : ο . x2)

as obj
cfe31..

as prop
-

theory
HoTg

stx
75b72..

address
TMNLY..^{ZermeloWOstrict}