law get_map

bend-mathlib@0.8.1.0 · list.bend:1715

import Base

1715# Indexing a map is mapping the indexed element.
1716law get_map:
1717  for ~A: Type
1718  for ~B: Type
1719  for ~f: A -> B
1720  for xs: List<A>
1721  for n: Nat
1722  {List.get(&1, B, List.map(~A, ~B, ~f, xs), n) == Maybe.map(&1, A, B, f, List.get(&1, A, xs, n)) : Maybe<&1, B>}