Proofgold Term Root Disambiguation

∀ x0 x1 . ordinal x0 ⟶ In x0 (Repl x1 (λ x2 . SetAdjoin x2 (Sing 1))) ⟶ False

as obj
-

as prop
e995a..^{ordinal_notin_tagged_Repl}

theory
HF

stx
8964b..

address
TMVD3..^{ordinal_notin_tagged_Repl}