a,b:, B:({a..b}Type).
  a<b  ((i:{a..b}B(i)) ~ ((i:{a..(b-1)}B(i))+B(b-1)))

1

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

3 steps

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