Nuprl - Proof: nsub inj exteq nsub surj 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub inj exteq nsub surj 1

1. k :

(

k inj

k) =ext (

k onto

By:	New:f (2 Times Analyze)

Generated subgoals:

1 2. f : k inj k
f k onto k
19 steps

2 2. f : k onto k
f k inj k
14 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

1	2. f : k inj k f k onto k	19 steps
2	2. f : k onto k f k inj k	14 steps