I have a goal with an existential variable ?x. In order to prove it, I need to destruct a term t, and under the different cases generated from destructing t, the term for instantiating ?x should be different in order to be correct.
When I finished proving the first case, Coq instantiate ?x based on my first case, which makes the second case not provable. Is there a way to turn a goal of the form P(?x) into exists x,P(x)?
Or are there other ways to solve the problem that I encounter?
An existential variable is merely a shortcut for a term you do not know how or want to write. In particular, it has only one instantiation, as in it stands for a fixed term that has only not yet been written explicitly. In particular, exists x, P x does not logically imply P ?x. In your case, I believe the solution is to never introduce ?x, i.e. avoid the tactic that introduced it (usually eapply).