Unclear error message when injectivity check fails in a subexpression

[jcp19]

The following example leads to a verification failure:

field Y_y: Bool
field X_y: Ref
predicate Inv(x: Ref) {
  acc(x.X_y) && (x.X_y != null ==> acc(x.X_y.Y_y))
}
predicate XsInv(xs: Seq[Ref]) {
  (forall i: Int, j: Int :: {xs[i], xs[j]} 0 <= i < j < |xs| ==> xs[i] != xs[j]) &&
  (forall i: Int :: {xs[i]} 0 <= i && i < |xs| ==> acc(Inv(xs[i])))
}
method f(xs: Seq[Ref])
  requires acc(XsInv(xs), write)
{
  unfold acc(XsInv(xs), write)

  // Below assertion fails
  assert forall i: Int, j: Int :: {xs[i], xs[j]} 0 <= i && i < j && j < |xs| ==>
    (unfolding acc(Inv(xs[i]), write) in true)
}

Error message:

Assert might fail. Assertion (forall i: Int, j: Int :: { xs[i], xs[j] } 0 <= i && (i < j && j < |xs|) ==> (unfolding acc(Inv(xs[i]), write) in true)) might not hold.

Adding the following assertion before the failing assertion reveals the true cause of the error

assert forall i: Int, j: Int :: {xs[i], xs[j]} 0 <= i && i < j && j < |xs| ==> acc(Inv(xs[i]), write)
// Error message: Assert might fail. Quantified resource Inv(xs[i]) might not be injective. (playground2.vpr@14.10--15.27)

It would be helpful to surface the injectivity errors in these cases.