In the book on page 81, chapter 7, section 7.3, Some Further Hints, there is a statement:
Don't assume values that look different are unequal.
The rules of TLA+ do not imply that 1 /= "a".
I need some explanations here. How? Why? I'm confused.