Nuprl - Proof: nsub surj least preimage works gen 1 2 1 2

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

1. B : Type
2. e : B

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

5. f :

B
6. Surj(

a; B; f)
7. y : B
8. (

x.(f(x)) e y)

{p:(

a. p(i) }
9. (f(least i:

. (f(i)) e y)) e y
10. f(least i:

. (f(i)) e y)

f(least i:

. (f(i)) e y)

By:	Inclusion -1

Generated subgoals:

None

About:

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