Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ or (x0 = 0) (∃ x1 . and (nat_p x1) (x0 = ordsucc x1))

as obj
-

as prop
4f416..^nat_inv

theory
HotG

stx
18c18..

address
TMa76..^nat_inv