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

1

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

5 steps

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