Recently, I attempted to generalize the fixed-point lemma and proved the following:

Let $ F_n $ be the set of formulas with $ n $ free variables in PA. Let $ \mu(x) $ be the smallest family of functions defined on $ F_n $ that satisfies:

$$ \ulcorner x \urcorner \in \mu(x) $$
$$\forall f_1(x) \forall f_2(x) \ldots \forall f_n(x) \in \mu(x) , ( \ulcorner x(f_1(x), f_2(x), \ldots, f_n(x)) \urcorner \in \mu(x) )$$ 

Then: for any $ \psi \in F_m $ and any set of $ n + m $ functions $ f_1(x), f_2(x), \ldots, f_{n+m}(x) \in \mu(x) $, there exists $ \varphi \in F_n $ such that:

$$ PA\vdash \varphi(f_1(\varphi), \ldots, f_n(\varphi)) \leftrightarrow \psi(f_{n+1}(\varphi), \ldots, f_{n+m}(\varphi)) $$

The proof itself is straightforward, but I am unsure under which existing research this result is covered, that is, what is the limit to which the fixed point lemma can be generalized? Recently, I have been reading C. Smorynski's article "Fixed Point Algebras." Am I heading in the right direction with my research?