Proofgold Term Root Disambiguation

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

as obj
-

as prop
7e47a..^SNoLev_PSNo

theory
HF

stx
8964b..

address
TMRD6..^SNoLev_PSNo