n,m:, f,g:(nm).
  (x:n, y:m. f(x,y) = g(x,y))
  
  sum(f(x,y) | x < n; y < m) = sum(g(x,y) | x < n; y < m)

By:	Auto THEN Unfold `double_sum` 0 THEN BackThru Thm* n:, f,g:(n). Thm* (i:n. f(i) = g(i))  sum(f(x) | x < n) = sum(g(x) | x < n) THEN BackThru Thm* n:, f,g:(n). Thm* (i:n. f(i) = g(i))  sum(f(x) | x < n) = sum(g(x) | x < n) THEN EasyHyp

None

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