Symbolic Logic - Question and answers

I'm working on a university project to create a proof checker for first-order logic. I've implemented rules like universal instantiation and modus ponens, but when I test with proofs that use existential elimination (e.g., from ∃x P(x), derive P(a) with a new constant), the system flags it as invalid even though it should be correct. I've double-checked my code for variable binding and scope, but I'm stuck. I'm using Python 3.9 and SymPy's logic module.