1. a : 
2. k : 
  (a {k} ) ~ (a {k} 2)

By:	At Type Witness: Wi(p,i. if p(i) 1 else 0 fi)  (a {k} )a {k} 2 | Wi(f,i. f(i)=1)  (a {k} 2)a {k}

1	(p,i. if p(i) 1 else 0 fi)  (a {k} )a {k} 2	2 steps
2	3. (p,i. if p(i) 1 else 0 fi)  (a {k} )a {k} 2   (f,i. f(i)=1)  (a {k} 2)a {k}	4 steps
3	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}    InvFuns(a {k} ;a {k} 2;p,i. if p(i) 1 else 0 fi;f,i. f(i)=1)	14 steps

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