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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub surj least preimage works gen 1 2 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. (

x.(f(x)) e y)

{p:(

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

. (f(i)) e y)) e y

f(least i:

. (f(i)) e y)

By:	ApFun: f to: least i:. (f(i)) e y

Generated subgoals:

1   (least i:. (f(i)) e y)  a
1 step

2 10. f(least i:. (f(i)) e y)  B
  f(least i:. (f(i)) e y)  B
1 step

About:

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

1	(least i:. (f(i)) e y) a	1 step
2	10. f(least i:. (f(i)) e y) B f(least i:. (f(i)) e y) B	1 step