This library deals with classical logic and its properties.
The main file is {\tt Classical.v}.

This library also provides some facts on an equality which contains its
own proof. See the file {\tt Eqdep.v}.

