1. k : 
2. 1<k
3. ((k-1)) ~ 
  (k) ~ ()

By:	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))) Using:[a:= 0 | b:= k | c:= k-1]

1

(((k-1))({(k-1)..k})) ~ ()

2 steps

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