T:Type, 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)

1

1. T: Type 2. P: T 3. L2: T List 4. u: T 5. v: T List 6. L1:T List. list_accum(l,x.if P(x) [x / l] else l fi;L1;v) ~ (rev(filter(P;v)) @ L1) 7. L1: T List 8. P(u) list_accum(l,x.if P(x) [x / l] else l fi;[u / L1];v) ~ (rev([u / filter(P;v)]) @ L1)

4 steps

About: