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-1). b(i))+b(a-1))

By:	Rewrite by Hyp:3 THEN Rewrite by Thm*  a,a':. a'-a = 1  (B:({a..a'}Type). (i:{a..a'}B(i)) ~ B(a))

1

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

1 step

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