law filter_append_sym

bend-mathlib@0.8.1.0 · list.bend:2518

import Base

2518# Filtering an append filters each part, reversed to rewrite toward the simple side.
2519law filter_append_sym:
2520  for ~A: Data
2521  for ~f: A -> Bool
2522  for xs: List<&2, A>
2523  for ys: List<&2, A>
2524  {List.append(&2, A, List.filter(~A, ~f, xs), List.filter(~A, ~f, ys)) == List.filter(~A, ~f, List.append(&2, A, xs, ys)) : List<&2, A>}