1. a : 
2. 0<a
3. b:((a-1)). (i:(a-1)b(i)) ~ ( i:(a-1). b(i))
4. b : a
  (i:ab(i)) ~ ( i:a. b(i))

By:	Use:[a:= 0 | b:= a | c:= a-1] Rewrite by Thm*  a,b:, c:{a...b}, B:({a..b}Type). Thm*  (i:{a..b}B(i)) ~ ((i:{a..c}B(i))+(i:{c..b}B(i)))

1

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

3 steps

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