Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ ordsucc (ordsucc x0) ⟶ ordsucc (mul_nat x1 x1) ∈ mul_nat (ordsucc (ordsucc x0)) (ordsucc (ordsucc x0))

as obj
-

as prop
87731..

theory
HotG

stx
33c6f..

address
TMJgR..