The Coq mailing list

[Justus Matthiesen <justus.matthiesen AT cl.cam.ac.uk>]

> A stripped down example of what I am trying to prove is :
> 
> c1 : C
> b1 : B
> ----------------------------------
> exists (c : C) (b : B), P c b
> 
> I would like to provide the witness b1 for b at this stage and provide a
> witness for c, different than c1, at a later moment. I tried "eexists;
> exists b1", but Coq didn't allow me to instantiate the existential variable
> created by eexists for c with anything else other than c1, which I don't
> want.

I'm sure there's better ways but my first idea would be to just prove that 
you 
are allowed to swap the quantifiers:

Lemma swap_exists {A B} {P : A -> B -> Prop} :
  (exists (b : B) (a : A), P a b) -> exists (a : A) (b : B), P a b.
Proof.
  firstorder.
Qed.


Justus