Does surjective pairing conservatively extend -conversion?

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

Do the surjective pairing axioms

$$\begin{aligned} D_{1}(Dxy) & = & x\\ D_{2}(Dxy) & = & y\\ D(D_{1}x)(D_{2}x) & = & x \end{aligned}$$

conservatively extend $\lambda\beta\eta$-conversion on pure untyped lambda
terms? More generally, is surjective pairing *always* conservative,
or do there exist lambda theories, or extensions of Combinatory Logic for
that matter, for which conservative extension by surjective pairing fails?
(Surjective pairing is conservative over the pure $\lambda\beta$-calculus;
see [&#91;Albert Meyer, 1991&#93;](<https://www.cs.tau.ac.il/~nachum/rtaloop/problems/5.html> "OpenTCS citation")). Of course, there are lots of other $\lambda\beta$,
indeed $\lambda\beta\eta$, theories where conservative extension holds,
simply because the theory consists of the valid equations in some
$\lambda$ model in which surjective pairing functions exist, e.g.,
$D_\infty$.

Recorded update.

Submitted by Kristian St{\o}vring on Tue, 22 Nov 2005 00:18:13 +0100. The problem has been solved with a positive answer~[Albert Meyer, 1991]. The generalization to arbitrary lambda theories remains open.