The Empty Type

The empty type is defined in the directory lib_empty.

 ** Module lib_empty Imports parameters
 $empty : Type(empty)
 $empty_elim : {C_empty:empty->TYPE}{z:empty}C_empty z
 ** Label (!empty!) empty
 ** Label (!empty elim!) empty_elim
  empty_rec = ... : {t|Type}empty->t
  empty_ind = ... : {P:empty->Prop}{z:empty}P z