The quantifier-elimination characterization for theories of tracial von Neumann algebras

Let $T$ be the theory of a tracial von Neumann algebra. A model $N$ of $T$ is of type I, and when $N$ has separable predual, projections $p,q\in N$ are conjugate by a trace-preserving automorphism exactly when $\tau(p)=\tau(q)$.

Quantifier-elimination conjecture. The following are equivalent:

1. $T$ admits elimination of quantifiers.
2. Every model $N$ of $T$ is of type I, and if $N$ has separable predual then two projections $p$ and $q$ in $N$ are conjugate by a trace-preserving automorphism if and only if $\tau(p)=\tau(q)$.

The conjecture is presented as a route toward a complete answer to Jekel's Question 2.18. The preceding proposition establishes the quantifier-elimination direction for a particular finite-dimensional setting, but the general equivalence remains unresolved in the supplied text.