law head_map

bend-mathlib@0.8.1.0 · list.bend:1662

import Base

1662# The head of a map is the mapped head.
1663law head_map:
1664  for ~A: Type
1665  for ~B: Type
1666  for ~f: A -> B
1667  for xs: List<A>
1668  {List.head(&1, B, List.map(~A, ~B, ~f, xs)) == Maybe.map(&1, A, B, f, List.head(&1, A, xs)) : Maybe<&1, B>}