law tail_map

bend-mathlib@0.8.1.0 · list.bend:1677

import Base

1677# The tail of a map is the map of the tail.
1678law tail_map:
1679  for ~A: Type
1680  for ~B: Type
1681  for ~f: A -> B
1682  for xs: List<A>
1683  {List.tail(&1, B, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~B, ~f, List.tail(&1, A, xs)) : List<B>}