WhoCites Definitions StandardLib Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites unique set?
unique_setDef {!x:T | P(x)} == {x:TP(x) & (y:TP(y y = x) }
Thm* T:Type, P:(TProp). {!x:T | P(x)}  Type

Syntax:{!x:T | P(x)} has structure: unique_set(Tx.P(x))

About:
setfunctionuniverseequalmember
propimpliesandall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

WhoCites Definitions StandardLib Sections NuprlLIB Doc