L:
List. sum(L[i]-1 | i < ||L||)+1- > L^1n,k:, c:(n
k). 
p:(k( List)). sum(||p(j)|| | j < k) = n & (j:k, x,y:||p(j)||. x < y 
(p(j))[x] > (p(j))[y]) & (j:k, x:||p(j)||. (p(j))[x] < n & c((p(j))[x]) = j)k:, f,g:(k
). (x:k. f(x)
g(x)) sum(f(x) | x < k)sum(g(x) | x < k)