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* P:(T), T':Type, f:({x:T| P(x) }T'), L1,L2:T List. mapfilter(f;P;L1 @ L2) = (mapfilter(f;P;L1) @ mapfilter(f;P;L2))	[mapfilter_append]
Def mapoutl(s) == mapfilter(x.outl(x);x.isl(x);s)	[mapoutl]

In prior sections: mb list 2

Try larger context: Graphs