The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

Hi there,

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.

Is there a better way to do this? Perhaps I didn't quite understand how existentials work in Coq?

Thanks,
Lucian