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
[[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