1. a : 
2. b : 
3. e : {a..b}
4. i : {a..b}
  e(i) | ( i:{a..b}. e(i))

By:	Rewrite by Thm*  a,c,b:, e:({a..b}). Thm*  ac Thm*   Thm*  c<b Thm*   Thm*  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))e(c)( i:{c+1..b}. e(i)) Using:[c:= i]

1

e(i) | ( i:{a..i}. e(i))e(i)( i:{i+1..b}. e(i))

1 step

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