law byte_xor
import lawful-words@0.1.0.0/proof_bytes.bend as ProofBytesimport Base
import lawful-words@0.1.0.0/defs.bend as D
635law byte_xor:
636 for +a: U32
637 for +b: U32
638 for +j: Nat
639 {D.byte(U32.xor(a, b), j) == U32.xor(D.byte(a, j), D.byte(b, j)) : U32}