Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ ∀ x1 : ι → ο . SNoLev (PSNo x0 x1) = x0

as obj
-

as prop
9c489..^SNoLev_PSNo

theory
HotG

stx
fab7c..

address
TMS4B..^SNoLev_PSNo