The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jeff Terrell wrote:
> I'd be grateful if someone would let me know why the last invocation 
> of "exists" fails, and what the error message
>
> "Not the right number of missing arguments (expected 0)"
>
> means in this context.

The goal there is a conjunction, not an existential quantification.  If 
you run [split] first, your [exists] works fine.

Presumably the error message has to do with Coq's attempt to treat 
conjunction as existential quantification.