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

By:	k:, b:, e:({a..b}). b-a = k  (( i:{a..b}. e(i)) = 0  (Or i:{a..b}. e(i) = 0)) Asserted THEN (UnivCD THEN Guarding (<prop>  <prop>) BackThru: Hyp:2 Using:[b-a])

1

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

6 steps

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