let mk_bwconj n a b = mk_bitwise n a b (mk_zero n)