is mentioned by

Thm* L: List. sum(L[i]-1 | i < ||L||)+1- > L^1	[Ramsey-base-case]
Thm* n,k:, c:(nk). 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)	[finite-partition]
Def array-count(v.P(v);a) == sum(if P(a[i]) 1 else 0 fi | i < |a|)	[array-count]

In prior sections: mb nat mb list 2 graph 1 1

Try larger context: Graphs