law drop_unpack

lawful-bytes@0.1.1.0 · proof_fast_find.bend:105

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

105law drop_unpack:
106  for +ws: List<&2, U32>
107  for +q: Nat
108  {List.drop(&2, U32, D.unpack(ws), Nat.mul(q, 4n)) == D.unpack(List.drop(&2, U32, ws, q)) : List<&2, U32>}