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