Should we not reuse constants in tableaux proofs?
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.