Set comprehension syntax

We want to use set comprehension to write sets and maps. There are some difficulties:

- The syntax keyword isn't powerful enough, but we could for example have a notation that has inverted binders
- Pattern matching is difficult to implement
- Constructing sets & maps also needs proofs that we can hopefully sometimes generate automatically