Nuprl - graph_1_1 LEMMAs for mapfilter

Rank	Theorem	Name
4	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]
cites
0	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]
3	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]