Def Unit == 0  

is mentioned by

Thm* P:(UnitProp). Dec(P())  Dec(x:Unit. P(x))

[decidable__ex_unit]

In prior sections: core bool 1 mb event system 3

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html