The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Li Long wrote:

> ..., but I was trying to prove the lemma
>  
> (forall x, (p -> q)) -> (p -> forall x, q), where x is not a free 
> variable of p,
>  

which I would state as
Goal forall A (p:Prop) (q:A->Prop), (forall x:A, p -> q x) -> (p -> 
forall x:A, q x).
Proof.
auto. (* easy proof: this lemma simply swaps the arguments of a binary 
function *)
Qed.

Bruno Barras.