is mentioned by

Thm* a,b,c:Top List. ((a @ b) @ c) ~ (a @ b @ c)	[append_assoc_sq]
Thm* n:, f,x:Top. primrec(n;x;f) ~ list_accum(i,y.f(y,i);x;upto(0;n))	[primrec_list_accum]
Thm* l1,l2:Top List, f,y:Top. list_accum(x,a.f(x,a);y;l1 @ l2) ~ list_accum(x,a.f(x,a);list_accum(x,a.f(x,a);y;l1);l2)	[list_accum_append]
Thm* L:Top List, n:{0...||L||}. (firstn(n;L) @ nth_tl(n;L)) ~ L	[append_firstn_lastn_sq]
Thm* f,g:Top, s:Top List. map(f;map(g;s)) ~ map(f o g;s)	[map-map]

In prior sections: mb list 1 mb basic

Try larger context: Graphs