WhoCites Definitions NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites sfa doc sexpr inj?
sfa_doc_sexpr_injDef Inj(a) == inr(a)
Thm* A:Type, a:A. Inj(a Sexpr(A)

Syntax:Inj(a) has structure: sfa_doc_sexpr_inj(a)

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

WhoCites Definitions NuprlPrimitives Sections NuprlLIB Doc