1. A : Type
2. A Discrete
3. k : 
4. f : kA
5. {a:A| i:k. a = f(i) }  Type
6. f  k{a:A| i:k. a = f(i) }
7. b : A
8. i:k. b = f(i)
9. e : AA
10. x,y:A. (x e y)  x = y
11. (j.(f(j)) e b)  {p:(k)| i:k. p(i) }
12. (least i:. (f(i)) e b)  k
  f(least i:. (f(i)) e b) = b  {a:A| i:k. a = f(i) }

By:	Inst: Thm*  k:, p:{p:(k)| i:k. p(i) }. p(least i:. p(i)) Using:[k | j.(f(j)) e b] THEN ReduceSOAps Hyp:-1

1

13. (f(least i:. (f(i)) e b)) e b   f(least i:. (f(i)) e b) = b  {a:A| i:k. a = f(i) }

3 steps

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