IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub inj exteq nsub bij1111 1. k : 2. f : kk 3. Inj(k; k; f)
4. fkk 5. Surj(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