The Coq mailing list

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

From: Adam Chlipala 
<adamc AT hcoop.net>
Subject: Re: [Coq-Club] case & inversion, Set & Prop
Date: Fri, 07 Aug 2009 13:49:42 -0400

> Keiko Nakata wrote:
> > As you know, I cannot prove a goal of the form "exists x, P" by 
> > coinduction.
> > So it sometimes happens that I need to construct x manually, then prove 
> > that
> > x indeed satisfies P by coinduction.
> >   
> 
> You might get some mileage out of defining a new co-inductive judgment 
> that combines [exists] and [P].  

Unfortunately I have not come up with such a mileage :(
But indeed when I got stuck by this problem, I was curious to know 
how one could devise such a new co-inductive judgment 
combining [exists] and [P]. And I am still curious about!

Best,
Keiko