The Coq mailing list

[gallais <guillaume.allais AT ens-lyon.org>]

Hi Lucian,

Is cut the tactics you are looking for? [cut C] will let you
assume that you have an inhabitant of [C] which you will
have to provide later on in your development.

Cheers,

--
gallais


On 4 December 2012 22:08, Lucian M. Patcas 
<lucian.patcas AT gmail.com>
 wrote:
> 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