The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Hello,

How can I instantiate an inner existential?

Suppose P and Q are of Prop and I have a subgoal :

exists i : Z, (P /\ (exists j : Z, Q))

I know that j does not depend on i and want to instantiate j first
with, say an integer 3, so as to make the subgoal look simpler.

It would be nicer if I can also instantiate j first with an object
which depends on i (e.g., i+3).  

With best regards,
Keiko