law slice_take

lawful-bytes@0.1.1.0 · proof_fast_append.bend:209

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

209# A slice of the first l elements, inside them.
210law slice_take:
211  for +xs: List<&2, U32>
212  for +l: Nat
213  for +q: Nat
214  for +n: Nat
215  for +h: {Nat.is_le(Nat.add(q, n), l) == True{} : Bool}
216  {D.slice(List.take(&2, U32, xs, l), q, n) == List.take(&2, U32, List.drop(&2, U32, xs, q), n) : List<&2, U32>}