如何在 Coq 中证明 (forall x, P x/\Q x) -> (forall x, P x)？已经尝试了几个小时，但不知道如何分解 Coq 可以消化的东西的前因。 (我是新手，显然:)
最佳答案
你可以通过应用 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.
关于proof - 如何证明 (forall x, P x/\Q x) -> (forall x, P x)，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/835183/