Proofgold Term Root Disambiguation

∀ x0 . not (0 = ordsucc x0)

as obj
-

as prop
c985e..^{neq_0_ordsucc}

theory
HF

stx
0d78c..

address
TMQSV..^{neq_0_ordsucc}