title: Dafny - Checking if array value is unique, but forall nested in exists not maintained by loop
body: <p>I'm checking if some key shows up only once in an array (where b is the the return value), however the following invariant says it isn't maintained by the loop:</p>
  
  <pre><code>invariant b &lt;==&gt; exists j | 0 &lt;= j &lt; i :: a[j] == key &amp;&amp; forall k | 0 &lt;= k &lt; i &amp;&amp; j != k :: a[k] != key
  </code></pre>
  
  <p>The loop continues as follows</p>
  
  <pre><code>  var i := 0;
    b := false;
    var keyCount := 0;
    while i &lt; a.Length
    invariant 0 &lt;= i &lt;= a.Length
    invariant b &lt;==&gt; exists j | 0 &lt;= j &lt; i :: a[j] == key &amp;&amp; forall k | 0 &lt;= k &lt; i &amp;&amp; j != k :: a[k] != key
    {
      if (a[i] == key)
      { keyCount := keyCount + 1; }
      if (keyCount == 1)
      { b := true; }
      else
      { b := false; }
      i := i + 1;
    }
  </code></pre>
  
  <p>The logic seems sound to me - is there something I'm missing?</p>