Use the current goal to determine. Return tt if the domain is ℤ, and return ff if it is ℕ
Attempts to discharge goals in the quantifier-free fragment of
linear integer and natural number arithmetic using the Omega test.
Guesses the correct domain by looking at the goal and hypotheses,
and then reverts all relevant hypotheses and variables.
Use omega manual to disable automatic reverts, and omega int or
omega nat to specify the domain.