Is this proof for showing that $EQ_{CFG}$ is co-Turing-recognizable incorrect?

Question

I have been searching for proofs that show that $EQ_{CFG}$ is co-Turing-recognizable. When searching for proofs I can only find proofs on the following form:

Construct a TM $M$ which recognizes the complement of $EQ_{CFG}$, M = "On input ⟨G,H⟩":

1. For each string $x \in \Sigma^*$ in lexicographic order:
2. Test whether x ∈ L(G) and whether x ∈ L(H), using the algorithm for $A_{CFG}$ .
3. If one of the tests accepts and the other rejects, accept; otherwise, continue.”

(From: http://cobweb.cs.uga.edu/~potter/theory/6_reducibility.pdf)

Isn't this proof incorrect?

Say that my language is $\Sigma=\{a,b\}$ and that I have $L(G_1) = \{b\}$ and $L(G_2) = {bb}$. $M$ should accept $\langle G_1, G_2\rangle$ since $L(G_1) \neq L(G_2)$. But if we run $M$ with $\langle G_1, G_2\rangle$ the TM will first generate $x=a$, which isn't in either languages so the machine will go back to step 1 and then generate $x=aa$, then $x=aaa$ and so on forever. The machine will never get to $x=b$. Hence, the machine will loop on input that it should accept. Therefore $M$ isn't a Turing recognizer.

Would the proof be correct if step 1 instead would state "For each string $x \in \Sigma^*$, ordered by increasing size and then lexicographic order:"? This should generate strings in the following order: $x=a$, $x=b$, $x=aa$, $x=ab$, $x=ba$, $x=bb$, $x=aaa$, and so on. So in the case above $M$ would reject when $x=b$.