1. A : Type
2. B : Type
3. f : AB
4. Surj(A; B; f)
5. a : 
6. s : aA
7. Surj(a; A; s)
8. B Discrete
9. f o s  aB
10. Surj(a; B; f o s)
11. e : BB
12. x,y:B. (x e y)  x = y
13. b : B
14. (i.((f o s)(i)) e b)  {p:(a)| i:a. p(i) }
15. (least i:. ((f o s)(i)) e b)  a
  ((f o s)(least i:. ((f o s)(i)) e b)) e b

By:	Use:[a | p(i):= ((f o s)(i)) e b] Inst: Thm*  k:, p:{p:(k)| i:k. p(i) }. p(least i:. p(i)) THEN Analyze THEN ReduceSOAps Concl

None

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