如何证明（forall x，P x / \ Q x）->（forall x，P x）

Question

如何在Coq中证明（forall x，P x / \ Q x）->（forall x，P x）？尝试了几个小时，无法弄清楚如何将前项分解为Coq可以消化的内容。（显然，我是新手：）

Answer 1

您只需应用H即可更快地完成此操作，但此脚本应该更清晰。

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.