Дафни: как использовать оба квантификатора вместе

Я пытаюсь использовать Dafny для проверки очень простого кода. Кулачный блок — обычная версия. И я просто не могу найти способ установить постусловие

"существует для всех j ~~~~~~"

Я не знаю, как использовать 2 квантификатора вместе в Dafny, помогите, пожалуйста. Спасибо.

//this is a c++ version of the code
for (int lastNot0 = 0, cur = 0; cur < nums.length; cur++) {
    if (nums[cur] != 0) {
        swap(nums[lastNot0 ++], nums[cur]);
    }
}

//Dafny code
method moveZero(a: array<int>)
  requires a != null && a.Length > 0;
  modifies a;
  ensures exists i :: forall j :: 0 <= j < i < a.Length && a[j] != 0;
//  ensures forall k :: 0 <= k < a.Length && k != i && k != j ==> a[k] == old(a[k]);
{
  var lastNot0 := 0;
  var cur := 0;
  while(cur < a.Length)
  invariant 0 <= lastNot0 <= cur < a.Length
  {
    if(a[cur] != 0){
      swap(a, lastNot0, cur);
      lastNot0 := lastNot0 + 1;
    }
    cur := cur + 1;

  }
}

method swap(a: array<int>, i: int, j: int)
  requires a != null && 0 <= i < j < a.Length;
  modifies a;
  ensures a[i] == old(a[j]);
  ensures a[j] == old(a[i]);
  ensures forall k :: 0 <= k < a.Length && k != i && k != j ==> a[k] == old(a[k]);
{
  var temp := a[i];
  a[i] := a[j];
  a[j] := temp;
}