Nuprl - Proof: nsub surj least preimage total gen 1 1 1 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 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
8. i :

9. i

0
10.

a. f(a) = y

a. f(i) = y

By:	SimilarTo: Hyp:-1

Generated subgoals:

None

About:

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