The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Jeff Terrell wrote:
> Is it possible to specify the name 'a' above (which appears to have 
> come from the induction step at the beginning of the proof) and the 
> name 'x' below (which is a witness of the existential quantification 
> above)?

Read about elimination patterns in the manual.  (You'll probably see 
them mentioned in the entries for [induction] and [destruct].)

> Could you explain the difference between simpl and (a possible 
> alternative) unfold In in this context. Both appear to do a similar 
> sort of thing (although one is more concise than the other), and both 
> work.

Have you read the manual entries on those tactics?