law bit_ext

lawful-words@0.1.0.0 · proof_u32.bend:1321

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

1321law bit_ext:
1322  for +a: U32
1323  for +b: U32
1324  for h: @k: Nat -> {D.bit(a, k) == D.bit(b, k) : Bool}
1325  {a == b : U32}