Proofgold Term Root Disambiguation

∀ x0 x1 . ordinal x0 ⟶ nIn (SetAdjoin x1 (Sing 1)) x0

as obj
-

as prop
c0e2c..^{tagged_notin_ordinal}

theory
HotG

stx
fab7c..

address
TMFQr..^{tagged_notin_ordinal}