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.

Observe that when you identify x with y, you are already drawing an equivalence between their formal representations (i.e. x, y), and the rule holds only for f that is blind to the formal representations, and distinguishes only between these equivalence classes. But within math topics there are notions of equivalence that are stronger than just that that the topic is uninterested in "piercing through the equivalence veil". For example, computer scientists often talk about Turing machines being equal even when their alphabets are disjoint, as long as their structure is the same, reserving equivalence typically to mean accepting the same language.

> Leibniz's rule

  > x=y  =>  f(x)=f(y)

Eh, it's useful in some cases, especially from a theoretical perspective, but...

  x = 0.0
  y = -0.0
  f = \x(copysign(1,x))
  
  x = "foo"
  y = "f"+"o"+"o"
  f = debug.dump-pointer

...pragmatically I'm not interested in a programming language where it does hold. It prohibits too many important utility functions.

You’re not even wrong. I suggest that you at least take the five minutes to read the wikipedia summary on predicate transformers before posting a replying in which you observably have no idea what you’re talking about.

Briefly, predicate transformers are functions about the behavior of a language, not functions in the language. In that model predicates are pure functions over the program state space and predicate transformers are functions from predicates to predicates. Clearly your objections are inapplicable.