IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub surj exteq nsub bij111 1. k :
2. f : kk 3. Surj(k; k; f)
4. fkk 5. Inj(k; k; f)
Bij(k; k; f)
By:
Def
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html