Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ omega ⟶ odd_nat (add_SNo 1 (mul_SNo 2 x0))

as obj
-

as prop
16a34..

theory
HotG

stx
8dd0d..

address
TMMym..