我正试图（经典地）证明
~ (forall t : U, phi) -> exists t: U, ~phi
在Coq。我要做的是证明它是相反的：
1. Assume there is no such t (so ~(exists t: U, ~phi))
2. Choose arbitrary t0:U
3. If ~phi[t/t0], then contradiction with (1)
4. Therefore, phi[t/t0]
5. Conclude (forall t:U, phi)
我的问题是第（2）和（5）行。我无法弄清楚如何 选择U的任意元素，证明一些事情 它，并总结一个forall。
任何建议（我不承诺使用对立面）？
为了模仿你的非正式证明，我使用经典公理¬¬P→P（称为NNPP）[1]。
申请后，你需要证明 False 具有A：¬（∀x：U，φx）和B：¬（∃x：U，φx）。 A和B是你推断的唯一武器 False。我们试试A [2]。所以你需要证明∀x：U，φx。为了做到这一点，我们采取任意t 0并试图证明φt0成立[3]。现在，由于你处于经典设置[4]，你知道φt0成立（并且它已完成[5]）或¬（φt0）成立。但后者是不可能的，因为它会与B [6]相矛盾。
Require Import Classical.
Section Answer.
Variable U : Type.
Variable φ : U -> Prop.
Lemma forall_exists:
~ (forall x : U, φ x) -> exists x: U, ~(φ x).
intros A.
apply NNPP. (* [1] *)
intro B.
apply A. (* [2] *)
intro t₀. (* [3] *)
elim classic with (φ t₀). (* [4] *)
trivial. (* [5] *)
intro H.
elim B. (* [6] *)
exists t₀.
assumption.
Qed.