law nth4_byte

lawful-words@0.1.0.0 · proof_bytes.bend:1283

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

1283law nth4_byte:
1284  for +w: U32
1285  for +j: Nat
1286  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
1287  {D.nth4(j, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)) == D.byte(w, j) : U32}