Our proof of model completeness for ACFA yields strong quantifier simplification results.
Let us start with a relative completeness result. If a theory $T$ is model complete, then whenever $E \models T$ and $E \subseteq M_i \models T$ for $i = 1$ and $2$, then $M_1 \equiv_E M_2$. For ACFA we can replace the condition $E \models T$ with just that $E$ is a substructure which is algebraically closed as a field.
Proposition: Let $(E,\sigma)$ be a difference field which is algebraically closed as a field. Suppose that $(E,\sigma) \subseteq (M_i,\sigma_i) \models \text{ACFA}$ are two extensions to existentially closed difference fields for $i = 1$ and $2$, then $M_1 \equiv_E M_2$.
Proof: Since $E$ is algebraically closed as a field, the ring $R := M_1 \otimes_E M_2$ is an integral domain (see Corollary 2 on page 202 of Nathan Jacobson, Lectures in Abstract Algebra III. Theory of Fields and Galois Theory, GTM 32.) and has a distinguished endomorphism $\sigma$ defined on tensors via $a \times b \mapsto \sigma_1(a) \otimes \sigma_2(b)$. Let $K := \mathcal{Q}(R)$ be the field of fractions of $R$ with $\sigma:K \to K$ the extension of $\sigma$ on $R$ defined by $\sigma(\frac{a}{b}) = \frac{\sigma(a)}{\sigma(b)}$. Let $(L,\sigma) \models \text{ACFA}$ be an existentially closed extension of $(K,\sigma)$. Then because ACFA is model complete, we have two elementary exrtenions $M_1 \preceq L$ and $M_2 \preceq L$. As $E$ is a common substructure of both $M_1$ and $M_2$, a fortiori, we have $M_1 \equiv_E L \equiv_E M_2$. $\Box$
Corollary: The completions of ACFA are in correspondence with pairs $(p,[\sigma])$ where $p$ is a prime number or $0$ and $[\sigma]$ is a conjugacy class in $\operatorname{Gal}(k_0^\text{alg}/k_0)$ with $k_0 = \mathbb{F}_p$ if $p$ is prime and $k_0 = \mathbb{Q}$ if $p = 0$.
Proof: For $(K,\sigma) \models \text{ACFA}$, let $\chi((K,\sigma)) := (p,[\sigma])$ where $p$ is the characteristic of $K$ and $[\sigma]$ is the conjugacy class of $\sigma \upharpoonright_{k_0^\text{alg}}$ with $k_0$ the prime field in $K$. As $K$ is algebraically closed, $k_0^\text{alg} \subseteq K$.
If $(K_i,\sigma_i) \models \text{ACFA}$ are models of ACFA for $i = 1$ and $2$ and $\chi((K_1,\sigma_1)) = \chi((K_2,\sigma_2))$, then $K_1$ and $K_2$ have a common prime field $k_0$ (as they have the same characteristic) and there is some $\tau \in \operatorname{Gal}(k_0^\text{alg}/k_0)$ with $\sigma_2 \upharpoonright_{k_0^\text{alg}} = \tau (\sigma_2 \upharpoonright_{k_0^\text{alg}} ) \tau^{-1}$. That is, $\tau:(k_0^\text{alg},\sigma_1 \upharpoonright_{k_0^\text{alg}} ) \to (k_0^\text{alg},\sigma_2 \upharpoonright_{k_0^\text{alg}} )$ is an isomorphism of difference fields. Set $E := (k_0^\text{alg},\sigma_1 \upharpoonright_{k_0^\text{alg}} )$. Then via the usual inclusion, $E$ is an algebraically closed substructure of $K_1$ and via $\tau$, it is an algebraically closed substructure of $K_2$. By the above proposition, $K_1 \equiv_E K_2$, which implies that upon forgetting $E$, we have $K_1 \equiv K_2$.
On the other hand, if $K_1$ and $K_2$ are models of ACFA with $K_1 \equiv K_2$, then clearly they have the same characteristic, and thus the same prime field $k_0$. As they are both algebraically closed, they both contain (copies of) $k_0^\text{alg}$. Thus to see that $\chi(K_1) = \chi(K_2)$ it suffices to show that for each finite Galois extension $L/k_0$ of $k_0$ there is an isomorphism $\tau:(L,\sigma_1 \upharpoonright_L) \to (L,\sigma_2 \upharpoonright_L)$, where here “$\sigma_i \upharpoonright_L$” means the restriction $\sigma_i$ to $L$ under some embedding of $L$ into $K_i$ for $i = 1$ and $2$. By the primitive element theorem, we may express $L = k_0[a]$ for some element $a \in L$. Let $P(x) \in k_0[x]$ be the minimal monic polynomial of $a$ over $k_0$. Then is a polynomial $Q \in k_0[x]$ so that $\sigma_1(a) = Q(a)$. As $K_1 \equiv K_2$, $K_2 \models (\exists b) (P(b) = 0 \land \sigma(b) = Q(b))$. Define $\tau:(L,\sigma_1 \upharpoonright_L) \to (K_2,\sigma)$ by $a \mapsto b$. A general element of $L$ may be expressed as $R(a)$ for some $R \in k_0[x]$. We compute that $\tau \sigma_1 (R(a)) = \tau (R(\sigma(a)) = \tau R(Q(a)) = R(Q(b)) = R(\sigma_2(b)) = \sigma_2(R(b))$. Thus, $\tau$ is an isomorphism of difference fields and in the direct limit we have an isomorphism $\tau:(k_0^\text{alg},\sigma_1 \upharpoonright_{k_0^\text{alg}}) \to (k_0^\text{alg},\sigma_2 \upharpoonright_{k_0^\text{alg}})$. That is, $\sigma_2 \upharpoonright_{k_0^\text{alg}} = \tau \circ \sigma_1 \upharpoonright_{k_0^\text{alg}} \circ \tau^{-1}$. $\Box$
Remark: It follows from the fact that Frobenius automorphism topologically generates $\operatorname{Gal}(\mathbb{F}_p^\text{alg}/\mathbb{F}_p)$ in characteristic $p$ and the Chebotarev density theorem in characteristic zero that for $k_0$ the prime field every difference field of the form $(k_0^\text{alg},\sigma)$ is isomorphic to the the algebraic closure of the prime field in $\prod_\mathcal{U} (\mathbb{F}_q^\text{alg},x \mapsto x^q)$ where $\mathcal{U}$ is a nonprincipal ultrafilter on the set of prime powers. In fact, in characteristic zero, we may assume that $\mathcal{U}$ is concentrated on the primes.
Proposition: If $(K,\sigma) \models \text{ACFA}$, $E \subseteq K$ is an algebraically closed substructure, and $a$ and $b$ are two tuples from $K$ of the same length, then $\operatorname{tp}(a/E) = \operatorname{tp}(b/E)$ if and only if there is an isomorphism of difference fields over $E$ between $E \langle a \rangle_{\sigma,\sigma^{-1}}^\text{alg}$ and $E \langle b \rangle_{\sigma,\sigma^{-1}}^\text{alg}$ taking $a$ to $b$ where the notation $E \langle a \rangle_{\sigma,\sigma^{-1}}$ means the inversive difference field generated by $a$ over $E$, that is, the field $E( \{ \sigma^j (a) : j \in \mathbb{Z} \})$ with the evident difference field structure.
Proof: For the forward direction, let $L \succeq K$ be an $|E|^+$-strongly homogeneous elementary extension of $K$. By strong homogeneity, if $\operatorname{tp}(a/E) = \operatorname{tp}(b/E)$, then there is an automorphism $\tau:L \to L$ fixing $E$ and taking $a$ to $b$. As $\tau$ is a map of difference fields, it takes $\sigma^j(a)$ to $\sigma^j(b)$ for all $j \in \mathbb{Z}$. Thus, $\tau$ maps $E \langle a \rangle_{\sigma,\sigma^{-1}}$ to $E \langle a \rangle_{\sigma,\sigma^{-1}}$, and thus anything algebraic over $E \langle a \rangle_{\sigma,\sigma^{-1}}$ to something algebraic over $E \langle b \rangle_{\sigma,\sigma^{-1}}$. That is, the restriction of $\tau$ to $E \langle a \rangle_{\sigma,\sigma^{-1}}^\text{alg}$ is an isomorphism of difference fields between $E \langle a \rangle_{\sigma,\sigma^{-1}}^\text{alg}$ and $E \langle b \rangle_{\sigma,\sigma^{-1}}^\text{alg}$ taking $a$ to $b$.
In the other direction, fix some isomorphism of difference fields $\tau:E \langle a \rangle_{\sigma,\sigma^{-1}}^\text{alg} \to E \langle b \rangle_{\sigma,\sigma^{-1}}^\text{alg}$ fixing $E$ and taking $a$ to $b$. Let $B := E \langle a \rangle_{\sigma,\sigma^{-1}}^\text{alg}$. Let $L_1 := L_2 := K$. Embed $B$ into $K_1$ via the usual inclusion and into $L_2$ via $\tau$. Then by our main proposition, $L_1 \equiv_B L_2$. Thus, for any formula $\phi(x) \in \mathcal{L}_E(x)$ where $x$ is a free variable of length equal to that of $a$, we have $K \models \phi(a) \Longleftrightarrow L_1 \models \phi(a) \Longleftrightarrow L_2 \models \phi(a) \Longleftrightarrow K \models \phi(\tau(a)) \Longleftrightarrow K \models \phi(b)$. That is, $\operatorname{tp}(a/E) = \operatorname{tp}(b/E)$. $\Box$
Corollary: If $K \models \text{ACFA}$, $k_0$ is the prime field in $K$, and $A \subseteq K$ is any subset, then $\operatorname{acl}(A) = k_0 \langle A \rangle_{\sigma,\sigma^{-1}}^\text{alg}$.
Proof: Set $E := k_0 \langle A \rangle_{\sigma,\sigma^{-1}}^\text{alg}$. Clearly, every element of $E$ is algebraic over $A$. Suppose that $b \in K \smallsetminus E$. Let $L := E \langle b \rangle_{\sigma,\sigma^{-1}}^\text{alg}$. Because $E$ is algebraically closed, for every $n$, the algebra $L^{\otimes n} = L \otimes_E L \otimes_E \cdots \otimes_E L$ is an integral domain with an endomorphism $\sigma$ defined on tensors by $a_1 \otimes \cdots \otimes a_n \mapsto \sigma(a_1) \otimes \cdots \otimes \sigma(a_n)$. Hence, it may be embedded into a difference field, and then into a model $(M,\sigma)$ of ACFA. The images of $b \otimes 1 \otimes \cdots \otimes 1$, $1 \otimes b \otimes 1 \cdots \otimes 1$, $\ldots$, $1 \otimes 1 \otimes \cdots \otimes b$ are distinct but the isomorphism between $L$ and its image where $x$ is mapped to the tensor $1 \otimes \cdots \otimes 1 \otimes x \otimes 1 \otimes \cdots \otimes 1$ where $x$ appears as the $m^\text{th}$ component shows by our last proposition that all of those elements have the same type over $E$ as $b$ itself. Thus, $b \notin \operatorname{acl}(E)$; showing that $E$ is model theoretically algebraically closed. $\Box$