Rationale: to make the code closer to what is on paper, I want the notations
to look like quantifiers, i.e. have a binder built-in. I thus introduced the
following notations:

  [★ map] k ↦ x ∈ m, P
  [★ set] x ∈ X, P

The good thing - contrary to the notations that we had before that required an
explicit lambda - is that type annotations of k and x are now not printed
making goals much easier to read.