law map_drop

bend-mathlib@0.8.1.0 · list.bend:1203

import Base

1203# Mapping commutes with dropping: map f (drop n xs) = drop n (map f xs).
1204law map_drop:
1205  for ~A: Type
1206  for ~B: Type
1207  for ~f: A -> B
1208  for xs: List<A>
1209  for n: Nat
1210  {List.map(~A, ~B, ~f, List.drop(&1, A, xs, n)) == List.drop(&1, B, List.map(~A, ~B, ~f, xs), n) : List<B>}