Proofgold Term Root Disambiguation

λ x0 . and (x0 ∈ omega) (∃ x1 . and (x1 ∈ omega) (x0 = mul_nat 2 x1))

as obj
c28a3..^even_nat

as prop
-

theory
HotG

stx
3b6f0..

address
TMJGQ..^even_nat