Term rewrite system for terms of lambda calculus?
I think that what you are looking for is called higher-order rewriting. There are systems in which you can define rewrite rules of the form $F\;(\lambda x.\lambda y.C\;X[x,y]) \longrightarrow X[X[t,u],v]$ for example, where $F$ and $C$ denote a function symbol and a constant symbols respectively. Note that here, $X$ denotes a higher-order variable (or meta-variable) of arity $2$. In the left-hand side (or pattern), it can be matched against any term containing only variables of $\{x,y\}$. The matched term is then used to replace the occurrences of $X$ in the right-hand side to apply the rewriting rule.

Note that the only terms that match the rewriting rule above are of the form $F\;(\lambda x.\lambda y.C\;A)$, with $FV(A) \subseteq \{x,y\}$. In this case, the variable $X$ is instantiated with $\hat{A}[-,-]$, which is a kind of context such that $A = \hat{A}[x,y]$.