law take_set

lawful-bytes@0.1.1.0 · proof_seq.bend:61

import Base

61law take_set:
62  for +xs: List<&2, U32>
63  for +m: Nat
64  for +i: Nat
65  for +v: U32
66  {List.take(&2, U32, List.set(&2, U32, xs, i, v), m) == List.set(&2, U32, List.take(&2, U32, xs, m), i, v) : List<&2, U32>}