Proofgold Term Root Disambiguation

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

as obj
-

as prop
83841..^{ordsucc_in_double_nat_ordsucc}

theory
HotG

stx
7fa67..

address
TMHXP..^{ordsucc_in_double_nat_ordsucc}