The Coq mailing list

[emily_p <emilypurfield AT gmail.com>]

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 have managed to solve the reverse of this but for this question I can't
seem to complete the proof. I can get to the stage where I have two subgoals
Px0 and Qx0 with the hypothesis forall x : S, Px^Qx but I am not sure how to
combine the goals to get a conjunction. I have used the following to get
this far but I may have gone down the wrong route completely.

intros. split. intro x0. 2: intro x0.

Thanks to anyone who can shed some light on this.

Emily
-- 
View this message in context: 
http://www.nabble.com/Proof-Help-tp23006221p23006221.html
Sent from the Coq mailing list archive at Nabble.com.