Proofgold Term Root Disambiguation

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

as obj
35592..^divides_nat

as prop
-

theory
HotG

stx
3b6f0..

address
TMFX8..^divides_nat