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. p : a
6. size(a)(p) = k
7. (i.if p(i) 1 else 0 fi=1) = p
  size(a)(i.if p(i) 1 else 0 fi=1) = k

1

size(a)(i.if p(i) 1 else 0 fi=1) = size(a)(p)

1 step

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