law map_map_sym

bend-mathlib@0.8.1.0 · list.bend:2261

import Base

2261# Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side.
2262law map_map_sym:
2263  for ~A: Type
2264  for ~B: Type
2265  for ~C: Type
2266  for ~f: A -> B
2267  for ~g: B -> C
2268  for xs: List<A>
2269  {List.map(~A, ~C, ~(x => g(f(x))), xs) == List.map(~B, ~C, ~g, List.map(~A, ~B, ~f, xs)) : List<C>}