def bit_dbl1
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire.bend as Lemireimport Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI
406def bit_dbl1(+y: Nat) -> {C.bit(1n+Nat.double(y)) == 1n : Nat}:
407 WI.bit_dbl(1n, y)