law get_set_ne

lawful-arrays@0.1.0.0 · proof_base.bend:411

import Base

411# Writing index i does not change index j != i.
412law get_set_ne:
413  for -A: Data
414  for +xs: List<&2, A>
415  for +i: Nat
416  for +j: Nat
417  for +v: A
418  for e: {Nat.is_eq(i, j) == False{} : Bool}
419  {List.get(&2, A, List.set(&2, A, xs, i, v), j) == List.get(&2, A, xs, j) : Maybe<&2, A>}