let mk_bwdisj n a b = mk_bitwise n a (mk_one n) b