Tenho um objetivo com uma variável existencial ?x. Para provar isso, preciso destruir um termo t e, nos diferentes casos gerados pela destruição de t, o termo para instanciar ?x deve ser diferente para ser correto.
Quando terminei de provar o primeiro caso, Coq instanciou ?x com base no meu primeiro caso, o que torna o segundo caso não demonstrável. Existe uma maneira de transformar um objetivo do formulário P(?x)em exists x,P(x)? Ou existem outras maneiras de resolver o problema que encontro?