Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . PNoEq_ x0 (λ x2 . x2 ∈ PSNo x0 x1) x1

as obj
-

as prop
68851..^PNoEq_PSNo

theory
HotG

stx
fab7c..

address
TMZtD..^PNoEq_PSNo