如何在Coq中证明以下目标？
Require Import Coq.Sets.Ensembles.
Goal (fun _ : nat => False) = Empty_set nat.
更新。我试过了
Proof.
apply functional_extensionality. intro n.
现在，我有以下子目标：
1 subgoal
n : nat
______________________________________(1/1)
False = Empty_set nat n
这个目标无法证明。尽管可以接受（它本身不会引起不一致），但这是不合时宜的结果。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句