law head_map_sym

bend-mathlib@0.8.1.0 · list.bend:2891

import Base

2891# The head of a map is the mapped head, reversed to rewrite toward the simple side.
2892law head_map_sym:
2893  for ~A: Type
2894  for ~B: Type
2895  for ~f: A -> B
2896  for xs: List<A>
2897  {Maybe.map(&1, A, B, f, List.head(&1, A, xs)) == List.head(&1, B, List.map(~A, ~B, ~f, xs)) : Maybe<&1, B>}