1. k : 
2. P : kProp
3. i:k. P(i)  [not for witness]
4. i:k. Dec(P(i))
  {i:k| P(i) & (j:i. P(j)) }

By:	Rewrite'-1 by Thm*  (x:T. Dec(E(x)))  (f:(T). x:T. f(x)  E(x)) THEN New:p Analyze-1

1

4. p : k 5. i:k. p(i)  P(i)   {i:k| P(i) & (j:i. P(j)) }

7 steps

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