def AP.pw_shln
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOFimport Base
422def AP.pw_shln(+d: Nat) -> {U32{AP.pw(32n, d)} == U32.shln(1, d) : U32}:
423 Equal.sym(U32, U32.shln(1, d), U32{AP.pw(32n, d)}, AP.shln_pw(d))
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOFimport Base
422def AP.pw_shln(+d: Nat) -> {U32{AP.pw(32n, d)} == U32.shln(1, d) : U32}:
423 Equal.sym(U32, U32.shln(1, d), U32{AP.pw(32n, d)}, AP.shln_pw(d))