law length_set_sym

bend-mathlib@0.8.1.0 · list.bend:2948

import Base

2948# Setting an element does not change the length, reversed to rewrite toward the simple side.
2949law length_set_sym:
2950  for -a: Quant
2951  for -A: Kind(a)
2952  for xs: List<a, A>
2953  for n: Nat
2954  for -x: A
2955  {List.length(a, A, xs) == List.length(a, A, List.set(a, A, xs, n, x)) : Nat}