law wbp3

lawful-bytes@0.1.1.0 · proof_core.bend:349

import Base
import lawful-words@0.1.0.0/defs.bend as W

349law wbp3:
350  for +w: U32
351  for +v: U32
352  for +hv: {U32.is_lt(v, 256) == True{} : Bool}
353  {L4(W.put_byte(w, 3n, v)) == List.set(&2, U32, L4(w), 3n, v) : List<&2, U32>}