law get_map_sym

bend-mathlib@0.8.1.0 · list.bend:2936

import Base

2936# Indexing a map is mapping the indexed element, reversed to rewrite toward the simple side.
2937law get_map_sym:
2938  for ~A: Type
2939  for ~B: Type
2940  for ~f: A -> B
2941  for xs: List<A>
2942  for n: Nat
2943  {Maybe.map(&1, A, B, f, List.get(&1, A, xs, n)) == List.get(&1, B, List.map(~A, ~B, ~f, xs), n) : Maybe<&1, B>}