law map_reverse_sym

bend-mathlib@0.8.1.0 · list.bend:2483

import Base

2483# Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs), reversed to rewrite toward the simple side.
2484law map_reverse_sym:
2485  for ~A: Type
2486  for ~B: Type
2487  for ~f: A -> B
2488  for xs: List<A>
2489  {List.reverse(&1, B, List.map(~A, ~B, ~f, xs)) == List.map(~A, ~B, ~f, List.reverse(&1, A, xs)) : List<B>}