is mentioned by

Thm* P:(T), a:array(T), i:|a|, v:T. array-count(v.P(v);a[i:=v]) = array-count(v.P(v);a)+if P(v)if P(a[i]) 0 else 1 fi ;P(a[i])-1 else 0 fi	[array-count-update]
Thm* T:Type, P:(T), a:array(T). array-count(v.P(v);a) (|a|+1)	[array-count_wf]
Thm* a:array(T), j,i:|a|, v:T. a[i:=v][j] ~ if j=i v else a[j] fi	[array-update-select]
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* k:, L: List. k-1- > L^k (i:||L||. L[i] < k)	[trivial-arrows]
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* n,m:, f:((n-1)(m-1)). Inj((n-1); (m-1); f) Inj(n; m; f[n-1:=m-1])	[fappend-inject]
Thm* n,m:, f:((n-1)(m-1)). increasing(f;n-1) increasing(f[n-1:=m-1];n)	[fappend-increasing]
Def path(the_graph;p) == 0 < ||p|| & (i:(||p||-1). p[i]-the_graph- > p[(i+1)])	[path]
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 mb basic mb nat mb list 1 mb list 2 graph 1 1 prog 1

Try larger context: Graphs