law map_append_sym

bend-mathlib@0.8.1.0 · list.bend:2249

import Base

2249# Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side.
2250law map_append_sym:
2251  for ~A: Type
2252  for ~B: Type
2253  for ~f: A -> B
2254  for xs: List<A>
2255  for -ys: List<A>
2256  {List.append(&1, B, List.map(~A, ~B, ~f, xs), List.map(~A, ~B, ~f, ys)) == List.map(~A, ~B, ~f, List.append(&1, A, xs, ys)) : List<B>}