The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

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].  It can be hard to "get back into the 
inductive world" from such a proof, but you can usually relate these 
proofs to inductive proofs in some way that mentions explicit depth bounds.