law take_split

lawful-bytes@0.1.1.0 · proof_fast_append.bend:180

import Base

180law take_split:
181  for +ys: List<&2, U32>
182  for +a: Nat
183  for +m: Nat
184  {List.append(&2, U32, List.take(&2, U32, ys, a), List.take(&2, U32, List.drop(&2, U32, ys, a), m)) == List.take(&2, U32, ys, Nat.add(a, m)) : List<&2, U32>}