1. a : 
2. k : 
  (p,i. if p(i) 1 else 0 fi)  (a {k} )a {k} 2

By:	Def of a {k}  | a {k} 2 THEN Analyze-1 THEN Analyze

1

3. p : a 4. size(a)(p) = k   Msize(i.if p(i) 1 else 0 fi) = k

1 step

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