law unpack_length

lawful-bytes@0.1.1.0 · proof_seq.bend:136

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

136law unpack_length:
137  for +ws: List<&2, U32>
138  {List.length(&2, U32, D.unpack(ws)) == Nat.mul(4n, List.length(&2, U32, ws)) : Nat}