n:
, R:(n
nProp), x,y:n. (x (R^*) y) 
(
k:(n+1). x R^k y)P:(Prop). (i:. (j:. j<i 
P(j)) P(i)) (i:. P(i))k,m:. (f:(km). Inj(k; m; f)) k
mR:(TTProp), k:, x,y:T.
Thm* (x R^k y)
Thm*
Thm* (
L:T List.
Thm* (||L|| = k+1
& L[0] = x & last(L) = y & (i:k. L[i] R L[(i+1)]))as,bs:T List. ||as @ bs|| = ||as||+||bs|| as,bs:T List, i:||as||. (as @ bs)[i] = as[i]as,bs:T List, i:{||as||..(||as||+||bs||)
}. (as @ bs)[i] = bs[(i-||as||)]as:A List, n:{0...||as||}. ||nth_tl(n;as)|| = ||as||-n as:A List, n:{0...||as||}. ||firstn(n;as)|| = n as:T List, n:{0...||as||}, i:(||as||-n). nth_tl(n;as)[i] = as[(i+n)]as:T List, n:{0...||as||}, i:n. firstn(n;as)[i] = as[i]