In some complicated proof, I end up trying to prove the following theorem, but I don't know how to do it:

```
Theorem exists_forall: forall (T: Type), exists (v: T), forall (d: T), d = v.
```

The challenge is that the `exists (v: T)`

appear before the `forall (d: T)`

part so eexists does not work.

Edit: I was able to prove it throught contradition in some of the other assuptions but I still wonder if this statement as it is:

A- is correct.

B- is provable

If a type T is empty, then it will be impossible to construct some v : T, unless Coq's whole logic is inconsistent.

There is an empty type built into the standard library, so this should be a counterexample.

Well, that is actually true, but we can simplify the problem as follows:

```
Theorem exists_forall: exists (v: nat), forall (d: nat), d = v.
```

This feels correct but it doesn't look provable because we need v to be equal to d, but d is not yet introduced.

It says that there is one natural number that all other natural numbers are equal to. This is only going to hold of one-inhabitant (up to propositional equality) types like `unit`

.

Last updated: Sep 28 2023 at 11:01 UTC