Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ not (atleastp (ordsucc x0) x0)

as obj
-

as prop
4fb58..^{Pigeonhole_not_atleastp_ordsucc}

theory
HotG

stx
84d03..

address
TMZSb..^{Pigeonhole_not_atleastp_ordsucc}