Quantify over ticked variables in rewrites?

[mtzguido]

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.