Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ο . PNoEq_ x0 x1 (λ x2 . and (x1 x2) (x2 = x0 ⟶ ∀ x3 : ο . x3))

as obj
-

as prop
52050..

theory
HoTg

stx
7f654..

address
TMWBZ..^{PNo_extend0_eq}