IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nsub inj exteq nsub bij
1
1. k : 
(k inj
k) =ext (k bij k)
| By: |
New:f (2 Times Analyze) |
Generated subgoals:
| 1 |
2. f : k inj k
f  k bij k
 | 3 steps |
| 2 |
2. f : k bij k
f k inj k
| 1 step |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
