Nuprl - Proof: nsub surj imp a rev inj gen 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. B : Type
2. e : B

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

5. f :

a onto

(

y.least x:

. (f(x)) e y)

B inj

By:	f a onto B Asserted THEN Analyze5

Generated subgoal:

1 5. f : aB
6. Surj(a; B; f)
7. f a onto B
(y.least x:. (f(x)) e y) B inj a
12 steps

About:

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