The one element type is defined in the directory lib_unit.
** Module lib_unit Imports lib_eq_basics $unit : Type(unit) $void : unit $unit_elim : {C_unit:unit->Type}(C_unit void)->{z:unit}C_unit z ** Label (!unit!) unit ** Label (!unit elim!) unit_elim ** Label (!unit void!) void [[C_unit:unit->Type][f_void:C_unit void] unit_elim C_unit f_void void ==> f_void] unit_rec = ... : {t|Type}t->unit->t unit_ind = ... : {P:unit->Prop}(P void)->{u:unit}P u is_void = ... : unit->Prop all_units_void = ... : {x:unit}is_void x all_units_same = ... : {x,y:unit}Eq x y