is mentioned by

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* k:, L: List, r1,r2:. r1r2 r1- > L^k r2- > L^k	[arrows-monotone1]
Thm* n,m:, f:(nm). Inj(n; m; f) nm	[pigeon-hole]
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 mb nat mb list 1 graph 1 1 core

Try larger context: Graphs