Should we not reuse constants in tableaux proofs?

I am trying to understand the proof of the following using tableaux:
$$
\exists x\forall y.r(x,y) \to \forall x \exists y . r(x,y)
$$

This is how it works out:
$$
(1) \space \exists x \forall y .r(x,y)
\\
(2) \space \lnot(\forall x \exists y . r(x,y))
\\
|
\\
(3) \space \forall y.r(a,y)
\\
(4) \space \lnot \exists y.r(b,y)
\\
(5) \space r(a,a)
\\
(6) \space r(a,b)
\\
(7) \lnot r(b,a)
\\
(8) \lnot r(b,b)
$$

I understand that (4) is derived from (2). However, shouldn't that be
$$
\lnot \exists y.r(a,y)
$$
reusing the constant a which was introduced by (3)? This is because we are expanding the quantifier:
$$
\lnot(\forall ...)
$$

Can anyone explain?

On the contrary, you never want to reuse constants. Each time you witness an existential quantifier, you should use a different constant. For example, consider the following two sentences:

-
Some integer is even.

-
Some integer is odd.

You wouldn't want to instantiate them with the same variable.

StackExchange Computer Science Q#24424, answer score: 2