The module lib_ML contains only one theorem which relates absurd in Prop with empty in SET
** Module lib_ML Imports lib_empty lib_unit lib_bool absurd_impl_empty = ... : absurd->empty
