[r0uv3n]

> ℤ ⊂ ℝ That is not at all obvious without some canonical isomorphism acting on ℤ, or at least is a behaviour strictly dependent on your particular set theoretic construction of the reals.

E.g. for the cauchy sequence construction of the reals, the image of the integer 1 under this canonical isomorphism would be the equivalence class of the sequence (1,0,0,0,...), but these are of course not the same object in a set theoretic sense.

[chiefjosh]

I think he literally just demonstrated the problem you were trying to illustrate about software provers