law byte_put_same

lawful-words@0.1.0.0 · proof_bytes.bend:872

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

872law byte_put_same:
873  for +w: U32
874  for +j: Nat
875  for +b: U32
876  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
877  for +hb: {U32.is_lt(b, 256) == True{} : Bool}
878  {D.byte(D.put_byte(w, j, b), j) == b : U32}