R:(Id
), in,out:(|R|IdLnk).
Thm* ring(R;in;out)
(
L:|R| List. 0<||L|| & (i:|R|. (i 
L)))n:
. ||upto(n)|| ~ nf:(AB), as:A List. ||map(f;as)|| = ||as|| 
a:T List, x:T', f:(TT'). (x map(f;a)) 
(y:T. (y a) & x = f(y))n,m:, f,i:Top. (f^n+m(i)) ~ (f^n(f^m(i)))n,i:. i<n (i upto(n))