Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ add_SNo (minus_SNo 1) (ordsucc x0) = x0

as obj
-

as prop
2f22f..^{add_minus_1_ordsucc}

theory
HotG

stx
5fba1..

address
TMPU9..^{add_minus_1_ordsucc}