Basic properties

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