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?