let mk_bwimp n a1 a2 = mk_bitwise n a1 a2 (mk_one n)