n:, f:(n), m,k:n.
  m = k
  
  (x:n. x = m  x = k  f(x) = 0)  sum(f(x) | x < n) = f(m)+f(k)

1

1. n :  2. f : n 3. m : n 4. k : n 5. m = k 6. x:n. x = m  x = k  f(x) = 0   sum(f(x) | x < n) = f(m)+f(k)

7 steps

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