Let's denote truth and false by two suitable constants $T, F$ where $T \not=_\beta F$ where $\equiv$ is syntactic identity.
Could I define a $\lambda$-term $E$ such that for $\lambda$-terms $X$ and $Y$ in $\beta\eta$-nf, where $X \not\equiv Y$
$E X X =_\beta T$ and $E X Y =_\beta F$?
Apologies for the delay on getting back to you. The following is not a complete answer, but it got a little long for a comment.
The reference I was thinking of was in Barendregt et al.'s Lambda Calculus with Types, Ch. 5.1. The reason this doesn't fully answer your question, though, is because it already assumes that, over and above the simply typed lambda calculus, you have universal quantification and implication, with equalities as atomic formulas. Here equality (at each type) seems to be a genuine predicate rather than a rewritability relationship.
With such a logic the addition of an identity operation (there a term $\delta_{A,B}$ with signature $A\times A\times B\times B\to B$) gives a system proof theoretically much stronger than the one without it. The reason being in essence that you can form terms like $\delta(\delta a_0a_1)(\delta a_2a_3)$ that tell you the identity of two identities, and other higher order fanciness. I am unfamiliar with the methods of figuring out relative strength of these sorts of systems, so I have little helpful to add beyond the above remarks. Still, the above chapter may be a good place to start.