A deep embedding for integers. Right now it only distinguishes natural numbers from general (unknown) integers.