law byte_put_other

lawful-words@0.1.0.0 · proof_bytes.bend:982

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

982law byte_put_other:
983  for +w: U32
984  for +i: Nat
985  for +j: Nat
986  for +b: U32
987  for +hb: {U32.is_lt(b, 256) == True{} : Bool}
988  for +hij: {Nat.is_eq(i, j) == False{} : Bool}
989  {D.byte(D.put_byte(w, j, b), i) == D.byte(w, i) : U32}