Much work has been done demonstrating that certain program transformations preserve particular properties. That is, for any program $P$ which has property $\alpha$, show that $P$ transformed under transformation $T$ still has property $\alpha$.
I'm interested in a transformation which replaces every usage of function $f$ in $P$ with partial function $g$, where $g$ is a restriction of $f$ (meaning that $g(x) = y \implies f(x) = y$). It seems intuitively obvious that this transformation, while not necessarily preserving totatlity, preserves partial correctness. Yet I cannot find a standard proof or reference on this or even mention of this seemingly elemental fact.
Can anyone help me out? A reference, a proof, a different formalism?