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