Proofgold Term Root Disambiguation

∀ x0 . not (ordsucc x0 = 0)

as obj
-

as prop
0610a..^{neq_ordsucc_0}

theory
HF

stx
0d78c..

address
TMPyF..^{neq_ordsucc_0}