rewrite each does not require equality

[mtzguido]

I was surprised by this second test succeeding, since it is just replacing i by j in the context and proving the equality between the resources (so foo i == foo j). But I would have expected that we check i == j. Doing that could also make the implementation of rewrite each more efficient, as it would involve a single query (instead of one per resource pair).

assume val foo : int -> vprop

```pulse
fn test1 (i j : int)
requires foo i ** pure (foo i == foo j)
ensures  foo j
{
  rewrite foo i as foo j;
}
```

```pulse
fn test2 (i j : int)
requires foo i ** pure (foo i == foo j)
ensures  foo j
{
  rewrite each i as j;
}
```

Calling this a bug, even though according to the documentation this is expected behavior (paraphrasing: "rewrite each e1 as e1' is equivalent to rewrite goal as goal' where goal' is computed by rewriting, in parallel, every occurrence of ei as ei' in goal.").

[mtzguido]

We agreed this is a quirk and should be changed. We may consider a construct to retain the old behavior, but the usual intention is that the equality is proven once and then substituted.