Nuprl - Proof: nsub surj imp a rev inj gen 1 1 1

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

1. B : Type
2. e : B

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

5. f :

B
6. Surj(

a; B; f)
7. f

a onto

(

y,x. (f(x)) e y)

{p:(

a. p(i) }

By:	Auto THEN Analyze THEN ReduceSOAps Concl

Generated subgoal:

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

About:

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