Add pattern variant of bind notation

Today I was looking for a pattern variant of stdpp's bind notation; my quick sketch ended up looking like:

Notation "' x ← y ; z" := (y ≫= (λ x : _, z))
  (at level 20, x pattern, y at level 100, z at level 200, only parsing) : stdpp_scope.

Example usage looks like '(existT aL NL) ← foo; bar. For clarity and to avoid conflicts, we could make the brackets part of the notation:

Notation "'( x ) ← y ; z" := (y ≫= (λ x : _, z))
  (at level 20, x pattern, y at level 100, z at level 200, only parsing) : stdpp_scope.

I'm not submitting a MR right now since I haven't fully debugged the notation and I ended up using some more custom notation.