law slice_split

lawful-bytes@0.1.1.0 · proof_fast_append.bend:197

import Base
import lawful-bytes@0.1.1.0/defs.bend as D

197law slice_split:
198  for +xs: List<&2, U32>
199  for +s: Nat
200  for +a: Nat
201  for +b: Nat
202  {List.append(&2, U32, D.slice(xs, s, a), D.slice(xs, Nat.add(s, a), b)) == D.slice(xs, s, Nat.add(a, b)) : List<&2, U32>}