This rises some more questions:
* How is equality/unequality defined actually?
** What about '1 = 2' and 1 /= 2?
** What about '1.0 = 1' and 1.0 /= 1?
** What about '3.14 = 1' and 3.14 /= 1?
As far as I know, every value is a set in TLA+.
We just don't care what the elmenets are in 1, 3.14 etc.
As far as I know, sets are equal if they have the same elements.
This means, that we can't compare sets of unknown elements.
* So what we can compare?
* Why Len() from Sequences works as expected?