1. a : 
2. k : 
3. (p,i. if p(i) 1 else 0 fi)  (a {k} )a {k} 2
4. (f,i. f(i)=1)  (a {k} 2)a {k} 
5. f : a {k} 2
  (i.if f(i)=1 1 else 0 fi) = f

By:	Analyze-1 THEN ((i.if f(i)=1 1 else 0 fi) = f  a2  Asserted THEN Analyze)

1	5. f : a2 6. Msize(f) = k   (i.if f(i)=1 1 else 0 fi) = f	2 steps
2	5. f : a2 6. Msize(f) = k 7. (i.if f(i)=1 1 else 0 fi) = f   Msize(i.if f(i)=1 1 else 0 fi) = k	3 steps

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