Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ SNoLev (minus_SNo x0) = x0

as obj
-

as prop
425f7..^{mordinal_SNoLev}

theory
HotG

stx
2cf07..

address
TMWf8..^{mordinal_SNoLev}