1. a : 
  k:, b:, e:({a..b}).
  b-a = k  (( i:{a..b}. e(i)) = 1  (And i:{a..b}. e(i) = 1))

1	2. b :  3. e : {a..b} 4. b-a = 0   ( i:{a..b}. e(i)) = 1  (And i:{a..b}. e(i) = 1)	2 steps
2	2. k :  3. 0<k 4. b:, e:({a..b}). 4. b-a = k-1  (( i:{a..b}. e(i)) = 1  (And i:{a..b}. e(i) = 1)) 5. b :  6. e : {a..b} 7. b-a = k   ( i:{a..b}. e(i)) = 1  (And i:{a..b}. e(i) = 1)	3 steps

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