Leibniz's rule does hold under these generalized notions of isomorphism and equivalence. Each of these notions implicitly sets apart some class of functions `f` as "not evil", i.e. as respecting Leibniz's rule wrt. that equivalence. So as long as your predicate transformers are not "evil" in that sense, you'll be covered. And in practice, trying to work with possibly "evil" functions without a clear notion of what equivalences would render them "not evil" is generally a waste of effort and leads to results that are not semantically useful.