Politeness suffices for theory combination

Let $\Sigma_1$ and $\Sigma_2$ be disjoint signatures, and let ${\mathcal{T}}_1$ and ${\mathcal{T}}_2$ be decidable theories over them. Let ${\mathcal{T}}_1\oplus{\mathcal{T}}_2$ be the theory over $\Sigma_1\cup\Sigma_2$ axiomatized by the union of the axioms of ${\mathcal{T}}_1$ and ${\mathcal{T}}_2$. A theory is polite when it is both smooth and finitely witnessable, where smoothness and finite witnessability are as defined in the source. Politeness conjecture. ${\mathcal{T}}_1\oplus{\mathcal{T}}_2$ is decidable, provided that ${\mathcal{T}}_2$ is polite. This conjecture asserts that politeness is sufficient for theory combination. It was stated as a theorem in earlier work, but the proof was later refuted; the claim consequently remained conjectural.