law tail_map_sym

bend-mathlib@0.8.1.0 · list.bend:2902

import Base

2902# The tail of a map is the map of the tail, reversed to rewrite toward the simple side.
2903law tail_map_sym:
2904  for ~A: Type
2905  for ~B: Type
2906  for ~f: A -> B
2907  for xs: List<A>
2908  {List.map(~A, ~B, ~f, List.tail(&1, A, xs)) == List.tail(&1, B, List.map(~A, ~B, ~f, xs)) : List<B>}