law byte_lt
import lawful-words@0.1.0.0/proof_bytes.bend as ProofBytesimport Base
import lawful-words@0.1.0.0/defs.bend as D
559law byte_lt:
560 for +w: U32
561 for +j: Nat
562 {U32.is_lt(D.byte(w, j), 256) == True{} : Bool}
import lawful-words@0.1.0.0/proof_bytes.bend as ProofBytesimport Base
import lawful-words@0.1.0.0/defs.bend as D
559law byte_lt:
560 for +w: U32
561 for +j: Nat
562 {U32.is_lt(D.byte(w, j), 256) == True{} : Bool}