Proofgold Term Root Disambiguation

∀ x0 . ordsucc x0 = add_nat x0 1

as obj
-

as prop
a7773..^{ordsucc_add_nat_1}

theory
HF

stx
e311e..

address
TMV3F..^{ordsucc_add_nat_1}