law get_set_ne

minebender-game@1.0.0.0 · proof_lists.bend:69

import Base

69law get_set_ne:
70  for -A: Data
71  for +xs: List<&2, A>
72  for +i: Nat
73  for +j: Nat
74  for +v: A
75  for e: {Nat.is_eq(i, j) == False{} : Bool}
76  {List.get(&2, A, List.set(&2, A, xs, i, v), j) == List.get(&2, A, xs, j) : Maybe<&2, A>}