The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Well, given a proof a of A and a proof f of forall x : A, P, you can 
build the proof f a of P[a/x].

Not sure if this answer your question, though.

Are you familiar with the Curry-Howard isomorphism? If not, I would 
advise to read about it.

Best,

Maxime.

On 08/06/2014 04:59 PM, Terrell, Jeffrey wrote:
> From a proof of A and a proof of A -> B, we can infer B. This is the 
> -> elimination rule.
>
> Similarly, from a proof a of A and a proof of forall x : A, P, we can 
> infer P[a/x]. This is the forall elimination rule.
>
> How are these elimination rules manifest in Coq?
>
> Regards,
> Jeff.