\section{Logic}\label{Logic}

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

This library also provides some facts on equalities for dependent
types. See the files {\tt Eqdep.v} and {\tt JMeq.v}.