Nuprl - Proof: nsub inj exteq nsub surj 1 2 1 1

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

1. k :

2. f :

k onto

k
3. f

k
4. Surj(

k; f)

Inj(

k; f)

By:	(New:X Analyze) THEN (New:a Analyze)

Generated subgoal:

1 5. X : k
6. a : k
7. f(X) = f(a)
X = a
11 steps

About:

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