In a higher-order pattern rewrite system, one specifies rewrites on beta normal forms of terms. Is it possible to have a rewrite like:
$\gamma := \lambda x . F(m) \to F(\lambda x . m)$
for some function symbol $F$ and $m$ in $\beta$-normal form? If so, then there is a "critical pair" between $\gamma$ and $\beta$
$F(m) [t/x] \leftarrow (\lambda x . F(m)) t \rightarrow (F(\lambda x .m )) t $
On the other hand, is there any reason to require $\gamma$ go the other direction?:
$F(\lambda x . m) \to \lambda x . F(m)$
This would avoid critical pairs with $\beta$, but may in practice be less natural.
If the former is possible, can one still conclude confluence if all critical pairs are development closed?