is mentioned by

Thm* L:T List. no_repeats(T;rev(L)) no_repeats(T;L)	[no_repeats_reverse]
Thm* x:T, L:T List. (x rev(L)) (x L)	[member_reverse]
Thm* P:(T), L2,L1:T List. list_accum(l,x.if P(x) [x / l] else l fi;L1;L2) ~ (rev(filter(P;L2)) @ L1)	[filter_list_accum]

In prior sections: list 1

Try larger context: Graphs