CODEWITHSUNDEEP
coq
Nastya Koroleva
Nastya Koroleva

Reputation: 73

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

Upvotes: 2

Views: 127

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33389

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.

Upvotes: 3

Related Questions