Quantifier bounds in set filters shouldn't allow multiple variables

[ahelwer]

This should be illegal:

---- MODULE Test ----
op == {x, y, z \in Nat : P(x, y, z)}
====

However, the quantifier_bound rule allows it. At the cost of making the set_filter rule more verbose this could be fixed, but making the grammar more restrictive often increases its size. Thus it is worth exploring whether fixing this is worth it.

Discovered in the course of working on https://github.com/tlaplus/tlaplus/issues/882

[ahelwer]

Note that CHOOSE has the same restriction, so perhaps we could abstract out the quantifier of that rule and merge it with the set filter rule.