let cofactors x a = match d_interp a with | Some(Bitwise _, [y;pos;neg]) when Term.eq x y -> (pos,neg) | _ -> (a,a)