is mentioned by

Thm* k:, L: List. 0 < ||L|| (r:. r- > L^k)	[Ramsey]
Thm* r,k:, L,R: List. 2k ||R|| = ||L|| (i:||L||. 0 < L[i] R[i]- > L[i--]^k) r- > R^k-1 r+1- > L^k	[Ramsey-recursion]
Thm* L: List, i,j:||L||. 0 < L[i] L[i--][j] = if j=i L[j]-1 else L[j] fi	[list-dec-select]
Thm* L: List, i:||L||. 0 < L[i] ||L[i--]|| = ||L||	[list-dec-length]
Thm* L: List, i:||L||. 0 < L[i] L[i--] List	[list-dec_wf]
Thm* L: List. sum(L[i]-1 | i < ||L||)+1- > L^1	[Ramsey-base-case]
Thm* k:, L: List, r1,r2:. r1r2 r1- > L^k r2- > L^k	[arrows-monotone1]
Thm* k:, L: List. k-1- > L^k (i:||L||. L[i] < k)	[trivial-arrows]
Thm* r:, k:, L: List. r- > L^k Prop	[arrows_wf]
Thm* n,m:, f:(nm). Inj(n; m; f) nm	[pigeon-hole]
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]
Thm* p:. prime(p) (m,n:. mm = pnn n = 0)	[sqrt_prime_irrational]
Def array(T) == n:nT	[array]
Def r- > L^k == n:. rn (G:({s:(n List)| ||s|| = k & (x,y:||s||. x < y s[x] < s[y]) }||L||). c:||L||, f:(L[c]n). increasing(f;L[c]) & (s:L[c] List. ||s|| = k (x,y:||s||. x < y s[x] < s[y]) G(map(f;s)) = c))	[arrows]

In prior sections: int 1 bool 1 int 2 num thy 1 list 1 sqequal 1 mb nat mb list 1 mb list 2 graph 1 1 prog 1

Try larger context: Graphs