Documentation Lacking for Multivar Set Comprehension

It appears to me that documentation for multivariable set comprehensions should be more easily accessible and detailed. My initial question was whether I could write something like:
{<<x,y>> : x \in 1..2, y \in 1..x}

The answer can of course be found in the operator semantics chapter of "Specifying Systems" (chapter, 16 page 301). But I think this feature is basic and useful enough, and the answer unintuitive enough I'd argue, that it should be, informally but clearly, documented elsewhere easily accessible, for instance Summary of TLA+.

And the answer is that rather than,
   {e : x \in X, y \in Y} == UNION {{e : y \in Y} : x \in X}
which would make the above _expression_ legal, it actually unfolds to,
   {e : x \in X, y \in Y} == UNION {{e : x \in X} : y \in Y}

The scope of variables is therefore defined from right to left. So the above should instead be written as,
{<<x,y>> : y \in 1..x, x \in 1..2}

NOTE: While this should work, it does not. The same bug affects multivar quantifiers. I reported it here https://github.com/tlaplus/tlaplus/issues/186

Back to the issue with the documentation though, other than the formal semantics in chapter 16 the only other references I found to multivar set comprehensions were:

* Summary of TLA+ (page 4):

https://lamport.azurewebsites.net/tla/summary-standalone.pdf

There's a reference to multivar in the footnotes, but doesn't clarify anything about scope.

* Specifying Systems, page 66

The semantics of multivar set comprehension are said to allow for the same generalisations as quantifiers do, without further detail. For quantifiers, "Specifying Systems", pag 14, informally defines:

\A x \in X, y \in Y : F == \A x in X : (\E y \in Y : F)

The semantics is quite clear in this case. But it is the opposite of set comprehensions with regards to scope. With quantifiers the scope is defined to from left to write. So in the above _expression_ x should be in the scope of Y.

NOTE: Again this should work but doesn't, see the above bug report.

\A x \in 1..2, y \in 1..x : TRUE

Let me end by noting that working without multivar can be a pain, more so with sets than quantifiers. Just compare the right-hand sides here,
\E x \in X, y \in Y, z \in Z : F == \E x \in X : \E y \in Y : \E z \in Z : F
and here,
{e : x \in X, y \in Y, z \in Z} == UNION {UNION {{e : x \in X} : y \in Y} : z \in Z}

The latter is quite horrible to both write and read.

So back to the point, I'd like to suggest that maybe the semantics of set comprehensions with multiple variables (and those of quantifiers for consistency) should be presented with more detail at least in the Summary of TLA+. Possibly also in the hyperbook. It should suffice to present the unfolding of a generic set comprehension with two variables, as done for quantifiers in page 14 of "Specifying Systems".