Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ or (x0 = 0) (∀ x1 : ο . (∀ x2 . and (nat_p x2) (x0 = ordsucc x2) ⟶ x1) ⟶ x1)

as obj
-

as prop
4f416..^nat_inv

theory
HotG

stx
18c18..

address
TMa76..^nat_inv