1. B : Type
2. e : BB
3. IsEqFun(B;e)
4. a : 
5. f : aB
6. Surj(a; B; f)
7. y : B
8. (x.(f(x)) e y)  {p:(a)| i:a. p(i) }
9. (f(least i:. (f(i)) e y)) e y
  (least i:. (f(i)) e y)  a

By:	BackThru: Thm*  k:, p:{p:(k)| i:k. p(i) }. (least i:. p(i))  k

None

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