is mentioned by

Thm* P:(T), T':Type, f:({x:T| P(x) }T'), L:T List, x,y:{x:T| P(x) }. x before y L f(x) before f(y) mapfilter(f;P;L)	[mapfilter_before]
Thm* f:(TT'), x,y:T, s:T List. x before y s f(x) before f(y) map(f;s)	[map_before]
Thm* L:T List, x,y:T. x before y L (L1,L2,L3:T List. L = (L1 @ [x] @ L2 @ [y] @ L3))	[l_before-iff]
Thm* L:T List, x,y:T. x before y L (A,B:T List. L = (A @ B) & (x A) & (y B))	[l_before_decomp]
Thm* A,B:T List, x,y:T. x before y A @ B x before y A x before y B (x A) & (y B)	[l_before_append_iff]

In prior sections: mb list 1 mb list 2

Try larger context: Graphs