You seem to be looking for the origin of a theorem that allows the simplification of a set of recursive definitions to a single recursive function definition. Apologies if I misread that. On with answering the question I think you asked.
The crucial year seems to be 1969. Three teams (where I take the liberty of calling some individuals teams) came up with important contributions to the theory of recursion as it matters to program semantics. As I helped to write elsewhere:
"In general, recursion appears in the form of a system of so-called
mutually recursive procedures, for instance, procedure $S$ with body
$P (S,T)$ and procedure $T$ with body $Q (S,T)$. The semantics of $S$
can now be expressed by $$\mu X.P (X,\mu Y.Q (X,Y))$$
and, similarly, $T$ is characterized by $$ \mu Y.Q (\mu X.P (X,Y),Y)~,$$
a result of [Bekic69][1], [Scott.deBakker69][2], and [Park70][3]."
[1]: Hans Bekic. Definable operations in general algebra, and the theory of automata and flow charts. Unpublished notes, IBM Laboratory Vienna, 1969.
[2]: Dana S. Scott and Jaco W. deBakker. A theory of programs. Seminar
notes, IBM Seminar, Vienna, 1969.
[3]: David M. R. Park. Fixpoint induction and proofs of program properties. Machine Intelligence, 5:59–78, 1969.
((a \/ c) ~> (b \/ c)) -> (a ~> b)
in generalized arrows for this purpose, I just couldn't realize it.) $\endgroup$ – polkovnikov.ph Feb 17 '18 at 15:08