Search code examples
proofcoq

How to prove (forall x, P x /\ Q x) -> (forall x, P x)

How does one prove (forall x, P x /\ Q x) -> (forall x, P x) in Coq? Been trying for hours and can't figure out how to break down the antecedent to something that Coq can digest. (I'm a newb, obviously :)

Solution

  • You can do it more quickly by just applying H, but this script should be more clear.

    Lemma foo : forall (A:Type) (P Q: A-> Prop), (forall x, P x /\ Q x) -> (forall x, P x).
intros.
destruct (H x). 
exact H0.
Qed.