Proofgold Term Root Disambiguation

λ x0 . and (x0 ∈ omega) (∀ x1 . x1 ∈ omega ⟶ x0 = mul_nat 2 x1 ⟶ ∀ x2 : ο . x2)

as obj
e1674..^odd_nat

as prop
-

theory
HotG

stx
3b6f0..

address
TMGKN..^odd_nat