The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

> I'm not qualified to answer to this part. But I don't think there is 
> anything general in that direction. There is a command Instantiate 
> (which is undocumented due to a rather poor syntax) which is intented to 
> solve this kind of  problems (finishing a proof which has uninstantiated 
> metavariables). Unfortunately, I can't seem to remember its syntax. If 
> someone does, it might possibly be useful as a temporary fix for your 
> proofs.

Instantiate (1 := ..) (in ..)

to replace the first existential variable.

Edsko