I'm having some trouble formally defining non-uniform substitution the replacement operation for a rule of replacement in propositional logic. Based on the idea of "Non-Uniform Substitution" from here (see section on Non-Uniform Substitution). Basically I'm trying to replace one or more instances of a subformula, as opposed to replacing all instances. This is needed for a toy deduction system I'm creating as an exercise, which basically allows substituting one or more instances of a subformula with its logical equivalent.
What I've tried so far:
Let $\phi$ be a formula. It's basically a string over the appropriate alphabet $\Sigma$, so we denote it as $t_{1} \ldots t_{n}$. We want $\phi[\overline{Q_{\theta|\psi}}|\overline{P}]$ to denote the formula resulting from replacing the sequence of subformulas $\overline{P}$ in $\phi$ (in that order) with another sequence $\overline{Q_{\theta|\psi}}$. Here, $\overline{Q_{\theta|\psi}}$ is just $\overline{P}$ with one or more instances of a subformula $\psi$ in $\overline{P}$ replaced by another formula $\theta$. Let $A$ be the set of atomic formulas and $\mathcal{L}$ be our language.
For my approach, I had to define the sequence $\overline{P}$ as a string and $p_1 \ldots p_n$ (same length as formula) where $p_i = *$ if $t_i \notin A$ and $p_i = t_i$ if $t_i \in A$. * is not part of $\mathcal{L}$ to avoid clashing with a legitimate symbol of $\mathcal{L}$.
Given $\phi$, construct a string $s_1 \ldots s_n$ where $s_i=t_i$ if $t_i \notin A$ and $s_i=q_i$ if $t_i \in A$ (Here $q_1 \ldots q_n$ represents the string $\overline{Q_{\theta|\psi}}$). Then the resulting string is the formula $\phi[\overline{Q_{\theta|\psi}}|\overline{P}]$.
The problem is this only allows me to replace atomic formulas of $\phi$ with other atomic formulas. I want to be able to replace any subformula of $\phi$ with another formula. Is there a better way of doing this?
EDIT: So what I'm after is actually called "Rule of Replacement" per Wikipedia. Anyone know a reference for a deduction system using rules of replacement (a formalized version)?