Possible new language constructs for TLA+3?

TLA+ as a language is pretty much perfect, but there are a couple scenarios where I wish for additional language constructs/features:

Combined set-builder notation

When defining a set with set-builder notation, we have two options:

Mapping: {f(x) : x \in S}
Filtering: {x \in S : p(x)}

I often find myself wanting to both map and filter at the same time, which requires the following somewhat cumbersome _expression_:

Map & Filter: {f(x) : x \in {y \in S : p(y)}}

I think this would be much improved in readability if we had a language-level construct similar to:

Combined: {f(x) : x \in S WHERE p(x)}

This is similar to set comprehensions in Python, which is probably my favorite feature of that language.

EXCEPT support for nested functions

Many of the specs I write are of distributed systems, so I'll usually have one or more variables of this type:

distributedData \in [Node -> [Key -> Value]]

When I want to update a single value in distributedData, I use this notation:

distributedData' = [distributedData EXCEPT ![node] = [@ EXCEPT ![key] = value]]

It would be nicer if we could write it something like this:

distributedData' = [distributedData EXCEPT ![node][key] = value]

I recall this also as a common point of confusion among TLA+ course attendees, who intuitively tried this notation at first.

I'm not sure whether either of these suggestions violate some bedrock principle in the TLA+ construction (I could see that for the latter) but they certainly would both make my life simpler and reduce the cognitive overhead of reading/writing TLA+.

New standard module: Query

Not a fully fleshed-out idea, but it might be nice to have a new standard module that implements something like relational algebra for easy manipulation of sets of records, in addition to other common higher-level functions like fold and zip.

Anyone else have suggestions of their own?