applying not giving permission incompleteness

[JonasAlaif]

The following fails to verify in Carbon (with "There might be insufficient permission to access y.f" inside the applying) but succeeds in Silicon

field f: Int
method m() {
  var x: Ref, y: Ref
  inhale acc(x.f) && (acc(x.f) --* acc(y.f))
  assert (applying (acc(x.f) --* acc(y.f)) in y.f == 0) || true
}