Theorem 12.1. $\mathrm{ACF}$ has quantifier elimination.