Definitions DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
exteqDef  A =ext B == (x:Ax  B) & (x:Bx  A)
one_one_corr_2Def  A ~ B == f:(AB), g:(BA). InvFuns(A;B;f;g)
Thm*  A,B:Type. (A ~ B Prop

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

Definitions DiscreteMath Sections DiscrMathExt Doc