Браво! Ты, как обычно, лучший! На самом деле это теорема

Пусть имеется терм C=C[f,m,n,k,...] содержащий (возможно) указанные свободные переменные. Тогда для произвольных термов M, N, K, ... существует терм F, такой что

F M N K ... = C[f:=F][m:=M][n:=N][k:=K]...

Доказательство - конструктивное, конструируется

F = Y(\fmnk... -> C[f,m,n,k,...])

и доказывается, что это то, что надо :)