law all_map_sym

bend-mathlib@0.8.1.0 · list.bend:2788

import Base

2788# All over a map checks the composed predicate: all p (map f xs) = all (p . f) xs, reversed to rewrite toward the simple side.
2789law all_map_sym:
2790  for ~A: Type
2791  for ~B: Type
2792  for ~f: A -> B
2793  for ~p: B -> Bool
2794  for xs: List<A>
2795  {List.all(~&1, ~A, ~(x => p(f(x))), xs) == List.all(~&1, ~B, ~p, List.map(~A, ~B, ~f, xs)) : Bool}