law map_drop_sym

bend-mathlib@0.8.1.0 · list.bend:2635

import Base

2635# Mapping commutes with dropping: map f (drop n xs) = drop n (map f xs), reversed to rewrite toward the simple side.
2636law map_drop_sym:
2637  for ~A: Type
2638  for ~B: Type
2639  for ~f: A -> B
2640  for xs: List<A>
2641  for n: Nat
2642  {List.drop(&1, B, List.map(~A, ~B, ~f, xs), n) == List.map(~A, ~B, ~f, List.drop(&1, A, xs, n)) : List<B>}