x=y →◊R(x,x)→◊R(x,y)
Similarly, the following ought to be derivable but isn't:x=y →◊⊤→◊x = y
The Leibniz' Principle as stated in the paper does not differentiate between modally existential formulae and modally universal. In an existential context x and y may be equal in this world and so in some successor worlds. Though we can't force equality, we also cannot prevent it. Thus, the Leibniz' Principle should allow for substitution of any number of existential occurrences of x by y, while other occurrences are still subject to the stricter rule (all or none may be replaced).