Proofgold Term Root Disambiguation

∀ x0 x1 . nat_p x1 ⟶ x0 ∈ ordsucc (add_nat x0 x1)

as obj
-

as prop
d8085..

theory
HotG

stx
a34e4..

address
TMHej..