Proofgold Term Root Disambiguation

∀ x0 x1 . ordinal x0 ⟶ nIn x0 {SetAdjoin x2 (Sing 1)|x2 ∈ x1}

as obj
-

as prop
e7ff3..^{ordinal_notin_tagged_Repl}

theory
HotG

stx
fab7c..

address
TMEiG..^{ordinal_notin_tagged_Repl}