def sc_take_update

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/list.bend:382

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

382def sc_take_update(-A: Data, +xs: List<&2, A>, +i: Nat, +v: A, +n: Nat) -> {SC.take(A, SC.update(A, xs, i, v), n) == SC.update(A, SC.take(A, xs, n), i, v) : List<&2, A>}:
383  match xs i n:
384    case Nil{} _ _:
385      {==}
386    case Con{a, t} 0n 0n:
387      {==}
388    case Con{a, t} 1n+j 0n:
389      {==}
390    case Con{a, t} 0n 1n+m:
391      {==}
392    case Con{a, t} 1n+j 1n+m:
393      cons_cong(A, a, SC.take(A, SC.update(A, t, j, v), m), SC.update(A, SC.take(A, t, m), j, v), sc_take_update(A, t, j, v, m))