law set_append_l

lawful-arrays@0.1.0.0 · proof_base.bend:350

import Base

350law set_append_l:
351  for -A: Data
352  for +xs: List<&2, A>
353  for +ys: List<&2, A>
354  for +i: Nat
355  for +v: A
356  for e: {Nat.is_lt(i, List.length(&2, A, xs)) == True{} : Bool}
357  {List.set(&2, A, List.append(&2, A, xs, ys), i, v)
358    == List.append(&2, A, List.set(&2, A, xs, i, v), ys) : List<&2, A>}