Should `with (bs). _` instantiate all binders?

The following fragment fails, perhaps puzzlingly to the user, since the `with y. _` eliminates only the first existential, so it is actually instantiated with `x`. This came up in a bigger module (by @utaal) where this was not so clear. Should we maybe check that we are eliminating all of the variables of an existential, and warn or fail if not?

Removing the `with` and `assert` makes this work, the issue is more about the behavior of `with`.

assume
val f : int -> vprop
assume
val g : int -> vprop

```pulse
fn test ()
requires exists* (x:int) (y:int). f y ** g x
ensures exists* (y:int) (x:int). f y ** g x
{
with y. _;
assert (f y);
();
}
```