 A wff of the form \(\exists \bx^1 \ldots \exists \bx^n [\bA=\bB]\) is a theorem of \(\cT\) iff there is a substitution \(\theta\) such that \(\theta \bA \conv \theta \bB\). In particular, \(\vdash \bA=\bB\) iff \(\bA \conv \bB\), which solves the decision problem for wffs of the form \([\bA=\bB]\). Naturally, the circumstance that only trivial equality formulas are provable in \(\cT\) changes drastically when axioms of extensionality are added to \(\cT\). \(\vdash \exists \bx_{\beta}[\bA=\bB]\) iff there is a wff \(\bE_{\beta}\) such that \(\vdash[\lambda \bx_{\beta}[\bA=\bB]]\bE_{\beta}\), but the decision problem for the class of wffs of the form \(\exists \bx_{\beta}[\bA=\bB]\) is unsolvable.