Existential Elimination (also called Existential Instantiation) says:
$$ \exists x[P(x)] \vdash P(c) \text{ For some c} $$
I was wondering whether it's bad form to use the same variable $x$ to conclude $P(x)$ for some $x$. I personally find it easier to read when the specific x that it was true for originally is pulled out. But perhaps there are pitfalls with reusing variable names after applying predicate rules?