1. a : 
2. k : 
3. 0<k
4. b:, e:({a..b}).
4. b-a = k-1  (( i:{a..b}. e(i)) = 1  (And i:{a..b}. e(i) = 1))
5. b : 
6. e : {a..b}
7. b-a = k
  ( i:{a..b}. e(i)) = 1  (And i:{a..b}. e(i) = 1)

By:	Rewrite by Thm*  f:(AAA), u:A, a,b:, e:({a..b}A). Thm*  a<b Thm*   Thm*  (Iter(f;u) i:{a..b}. e(i)) = f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) THEN Reduce Concl

1

( i:{a..b-1}. e(i))e(b-1) = 1  (And i:{a..b-1}. e(i) = 1) & e(b-1) = 1

2 steps

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