Invariant in linear search?

Question

Algorithms

There is a linear search algorithm

A = {1, 2, 7, 5, 8}
v = 7

def search(A, v)
    i = 0
    while i < A.length do
        if A[i] == v then
            return i
        end
        i++
    od
    return nil
end

A - set of elements
i - index of the current element
v - element we are looking for

Is it true that the invariant will be:
1. A[i] ∈ A
2. i ∈ {0, ...A.length - 1} or i ∈ {}

Answer 1

1. A[i] ∈ A
2. i ∈ {0, ...A.length - 1} or i ∈ {}

As for me, such an invariant will be somewhat useless, since it does not allow proving the correctness of the algorithm (by induction). Also, "or i ∈ {}" is an even more useless addition to the condition, because, although it does not make the invariant incorrect, it makes it weaker, because inside the cycle (and after it) there is always some number in i.
IMHO, a good invariant:
The elements of A with indices up to [i-1] inclusive do not contain v.