1. a : 
2. 0<a
3. b:((a-1)). (i:(a-1)b(i)) ~ ( i:(a-1). b(i))
4. b : a
  ((i:(a-1)b(i))+(i:{(a-1)..a}b(i))) ~ ( i:a. b(i))

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

1

((i:(a-1)b(i))+(i:{(a-1)..a}b(i))) ~ (( i:(a-1). b(i))+b(a-1))

2 steps

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