Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ SNoCutP (SNoS_ x0) 0

as obj
-

as prop
0cfe8..^{ordinal_SNoCutP}

theory
HotG

stx
2cf07..

address
TMW1U..^{ordinal_SNoCutP}