Remark Definitions StandardLib Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
No other cites to report in StandardLib
type_injDef [x]{T} == x
Thm* T:Type, E:(TTProp).
Thm* (EquivRel x,y:TE(x,y))  (a:T. [a]{x,y:T//E(x,y)}  x,y:T//E(x,y))

Syntax:[x]{T} has structure: type_inj(xT)

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

Remark Definitions StandardLib Sections NuprlLIB Doc