Extend combination results on rewrite orderings to systems involving reductions.

The source page states the original problem together with its recorded qualifications and progress updates as follows.

A collection of rewrite orderings operating on disjoint signatures can be extended to an ordering operating on the union of the signatures, while still preserving part of the properties [Jouannaud, 1995]. Such constructions can be used for proving modular termination properties of rewrite systems. Do they extend to the case where one of the starting orderings is given by $\beta\eta$ reductions on typed lambda terms?