Proofgold Term Root Disambiguation

∀ x0 . ordinal x0 ⟶ x0 = SNoCut (SNoS_ x0) 0

as obj
-

as prop
1f113..^{ordinal_SNoCut_eta}

theory
HotG

stx
2cf07..

address
TMSVc..^{ordinal_SNoCut_eta}