1. P : Prop
2. i:. P(i)  [not for witness]
3. i:. Dec(P(i))
  {i:| P(i) & (j:. 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

3. p :  4. i:. p(i)  P(i)   {i:| P(i) & (j:. j<i  P(j)) }

7 steps

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