Dafny error proving assertion on an unmodified array

The below Dafny method simply asserts that for every index i, there exists an index j such that the input array elements are equal. I am curious why the particular invariant and assertion does not hold since I am not modifying the array. Isn't supposed to be obvious to the Dafny? Am I missing something.

method test(a:array<int>) returns (b:array<int>)
requires a.Length > 0
ensures b.Length > 0
ensures a.Length == b.Length
ensures forall k: int::0 <= k < a.Length ==> b[k] == a[k]
{
    var i:= 0;
    var j := 0;

    while i < a.Length
    invariant i >=0 && j>=0
    invariant i==j
    invariant i <= a.Length && j <= a.Length
    invariant forall k: int::0 <= k < i ==> exists l | 0 <= l < j:: a[k] == a[l]
    decreases (a.Length - i)
    decreases (a.Length - j)
    {
       assert forall k: int::0 <= k < i ==> exists l | 0 <= l < j:: a[k] == a[l];
       i := i+1;
       j := j+1;
    }
    return a;
}

I tried to put assertions at different points in the while loop but with no result. I think this is a simple program that reads the input array. In the worst case, i == j. But for some reason that I don't understand, the verification fails.

Any insight into why it fails and a possible hint on how to proceed will help. Note that I do want to retain the invariant using exists

Here is a version that asserts the loop invariant after the loop. It differs to the previous versions in that it externalises the predicate used within the universal quantification. Quantifiers are a common source of unintuitive behaviour and this workaround typically helps with such issues.

predicate P(a: array<int>, k: int, i: int)
reads a
requires i <= a.Length
requires 0 <= k < i
{
    exists l | 0 <= l < i :: a[k] == a[l]
}

method test(a:array<int>) returns (b:array<int>)
requires a.Length > 0
ensures b.Length > 0
ensures a.Length == b.Length
ensures forall k: int | 0 <= k < a.Length :: b[k] == a[k]
{
    var i:= 0;
    var j := 0;

    while i < a.Length
     invariant i >= 0 && j >= 0
     invariant i == j 
     invariant i <= a.Length && j <= a.Length
     invariant forall k: int | 0 <= k < i :: P(a, k, i)
     decreases (a.Length - i)
     decreases (a.Length - j)
    {
       assert a[i] == a[j];
       i := i+1;
       j := j+1;
    }
    assert forall k: int | 0 <= k < i :: P(a, k, i);
    return a;
}