Proofgold Term Root Disambiguation

∀ x0 x1 . nat_p x1 ⟶ ordsucc (96eca.. x0 x1) ∈ x0 ⟶ 96eca.. x0 (ordsucc x1) = ordsucc (96eca.. x0 x1)

as obj
-

as prop
ac69f..

theory
HotG

stx
33c6f..

address
TMcUH..