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

By:	Guarding (<prop>  <prop>) (NatInd Concl)

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

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