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
The module lib_nat_Lt_ML contains elimination rules for nat .
** Module lib_nat_Lt_ML Imports lib_ML lib_nat_Lt complete_elimination = ... : {P:nat->Type}({n:nat}({x:nat}(Lt x n)->P x)->P n)->{m:nat}P m well_founded_elimination = ... : {t|Type}{f:t->nat}{P:t->Type} ({x:t}({y:t}(Lt (f y) (f x))->P y)->P x)->{z:t}P z