law unpack_length4

lawful-bytes@0.1.1.0 · proof_seq.bend:124

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

124law unpack_length4:
125  for +ws: List<&2, U32>
126  {List.length(&2, U32, D.unpack(ws)) == Nat.mul(List.length(&2, U32, ws), 4n) : Nat}