Proofgold Term Root Disambiguation

∀ x0 x1 . ordinal x0 ⟶ SNo_ x0 x1 ⟶ x1 = PSNo x0 (λ x3 . x3 ∈ x1)

as obj
-

as prop
63011..^{SNo_PSNo_eta_}

theory
HotG

stx
fab7c..

address
TMcuW..^{SNo_PSNo_eta_}