The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

fdabrows AT irisa.fr
 wrote:
> > Hello,
> >
> > I am fairly new to Coq and I am not sure if this is the right place to
> >     
> ask but I am hoping someone can help me. I am having trouble with what I
> think should be a simple proof. I am trying to solve the following
>   
> > forall x, P x^Q x |- (forall x Px) ^(forall x Qx)
> >     

I feel like I should jump in and bring up that the built-in [firstorder] 
tactic solves this goal, so that's the right way to do it in real 
developments. ;-)