law get_set_self_sym

bend-mathlib@0.8.1.0 · list.bend:2960

import Base

2960# Reading the index just set gives the new value wherever the index is in range, reversed to rewrite toward the simple side.
2961law get_set_self_sym:
2962  for -a: Quant
2963  for -A: Kind(a)
2964  for xs: List<a, A>
2965  for n: Nat
2966  for -x: A
2967  {Maybe.map(a, A, A, y => x, List.get(a, A, xs, n)) == List.get(a, A, List.set(a, A, xs, n, x), n) : Maybe<a, A>}