Search code examples
coq

How to prove `(fun _ : nat => False) = Empty_set nat` in Coq?

How can I prove the following goal in Coq?

Require Import Coq.Sets.Ensembles.

Goal (fun _ : nat => False) = Empty_set nat.

Update. I've tried

Proof.
   apply functional_extensionality. intro n.

now I have the following subgoal:

1 subgoal
n : nat
______________________________________(1/1)
False = Empty_set nat n
Solution

  • This goal cannot be proved. It can be admitted though (it does not introduce an inconsistency on its own), and it is a consequence of univalence.