method IndexOf(a: array<int>, x: int) returns (i: int)
  ensures (i == -1 && x !in a[..]) || (0 <= i < a.Length && a[i] == x && 
                                         (forall j | 0 <= j < i :: a[j] != x))
{
    // return -1;
    i := 0;
    while i < a.Length 
      invariant i <= a.Length && x !in a[0..i]
    {
        if a[i] == x {  // ! (should be x)
            return i;
        }
        i := i + 1;
    }
    // ?/????????????????
    assert i >= a.Length;
    assert i == a.Length;
    // assert x !in a[..];
    return -1;
}

method Main() {
    var a := new int[] [5, 5, 2, 10];
    var i := IndexOf(a, 5);
    assert i != -10;
    assert a[0] == 5;
    assert a[1] == 5;
    assert 5 in a[..];
    assert i == -1     ==>    5 !in a[..];
    assert i != -1;
    assert i == 0;
    print i, "\n";
}