Nuprl - Proof: nsub surj least preimage total gen 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub surj least preimage total gen 1 1 1 1

1. B : Type
2. e : B

3. IsEqFun(B;e)
4. a :

5. f :

B
6. Surj(

a; B; f)
7. y : B

a. (f(i)) e y

By:	Witness4: y

Generated subgoal:

1 8. i :
9. i0
i:a. (f(i)) e y
3 steps

About:

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