Sometimes you just want to prove that nasty ~ T = U for some types T and U. Well, while in general it is not decidable (nor provable), sometimes there is a relatively easy way to do it, when T and U are not both infinite. In other words, either T or U, or both of them should be finite.

# Simple example: bool is not unit

The idea is simple: if types are equal, there exists a bijection between their elements. Let us prove a simple lemma exists_bijection:

The proof was a piece of cake. Now to battle!

You remember, that unit is a type, inhabited by only one element tt?

Both f true and f false are evaluated to tt. There is not much choice here. However we know, that $\forall x, (g \cdot f) \ x = x$ . By instantiating x with true and false we get $g (f \ true) = true$ and $g (f \ false) = false$. Since both $f \ true$ and $f\ false$ are equal, we deduce $g\ tt =true$ and $g \ tt = false$, contradiction.

Here is a little diagram to help:

Now the code:

So, the key idea is to enumerate possible bijections. As at least one of sets is finite, you will eventually enumerate all the candidates, and when the sets are of different size, you will get contradictions because you will run out of distinct functions trying to enumerate all bijections.

## Example: nat is not bool

Let us apply the same principle to prove ~ nat = bool.

We are going to use a bit of semicolons because otherwise the proof will become very repetitive. Basically where you see an exclamation mark we got 8 goals which contexts include:

where x, y, z all range over ${ true, false}$. There will always be at least two of three boolean values equal to each other (which should follow from Dirichlet principle), which will feed us with nice contradiction to do a rewrite and inversion.

An interesting question (the answer to which I do not know) is whether we could automate it inside Coq somehow without writing plugins for it.