coq - 如何在 Coq 中证明 `(fun _ : nat => False) = Empty_set nat`？

Question

如何在 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

标签： coq

Answer 1

这个目标无法证明。虽然它可以被承认（它本身不会引入不一致），它是单价的结果。