Quantify over ticked variables in rewrites?

```fstar
fn test (r1 r2 : ref int)
requires pts_to r1 'x ** pure (r1 == r2)
ensures pts_to r2 'x
{
rewrite pts_to r1 'y as pts_to r2 'y;
}
```
I think it would be nice if this worked, by quantifying over `'y` with a `with`. Note that it does work if we say `'x`, but that's just referring to the implicitly-quantified `'x` above.

Not sure if this would raise more confusion though.