# On the empty set

Prove the following two propositions, which only *apparently*
contradict each other:
Theorem all_equal : forall x y : Empty_set, x = y.
Theorem all_diff : forall x y : Empty_set, x <> y.

## Solution

Look at this file

Going home

Pierre Castéran