Proofgold Term Root Disambiguation

∀ x0 x1 . not (x0 = x1) ⟶ not (ordsucc x0 = ordsucc x1)

as obj
-

as prop
aaf17..^{ordsucc_inj_contra}

theory
HF

stx
0d78c..

address
TMHv7..^{ordsucc_inj_contra}