Def sum(f(x) | x < k) == primrec(k;0;x,n. n+f(x))

is mentioned by

Thm* n:, f:(n), p:(nn). Thm* Bij(n; n; p)  sum(f(p(x)) | x < n) = sum(f(x) | x < n)

[permute_sum]

In prior sections: mb nat

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html