The result can be proved using the standard textbook proof of the Cook-Levin theorem. The key observation is that the 3CNF produced by the reduction in the proof of Cook-Levin is very regular and therefore compressible. There is a sketch in Ryan's "casual" presentation of his circuit lower bound (Thm. 2.2.). Below I am summarizing the argument.
By definition, a language $L$ is in $\mathsf{NEXP}$ if there exists a (single tape) nondeterministic Turing machine $M_L$ that on input $x$ outputs $1$ if and only if $x \in L$, and runs in time bounded by $2^{p(|x|)}$. For any $x$ we can think of a tableau of the computation of some accepting path of $M_L$: make a table of size $2^{p(|x|)} \times 2^{p(|x|)}$ and in cell $(i, j)$ write down the contents of the $j$-th cell of the tape at time step $i$ (at time step 1 we assume the tape contains $x$ and at the final time step we want the tape to only contain 1, indicating acceptance). Also, there is a special symbol where the head of the Turing machine is at each time step, and the internal state is also indicated in that cell. So the question "does there exist an accepting path of $M_L$ for $x$" boils down to "can we fill out the tableau for $x$ correctly according to the transition table of $M_L$?" The main idea of Cook-Levin is that whether the tableau is filled out correctly can be checked by verifying a number of local constraints, because each cell of the tableau only depends on the three cells above it. Thus each local constraint can be checked by a constant size 3CNF and the conjunction of the 3CNFs is the formula $f(x)$. The new observation for the $\mathsf{NEXP}$ version is that, except for the first $|x|$ entries of the first row and the first entry of the last row of the tableau (where we check that the tape starts off with containing $x$ and ends with containing $1$), each 3CNF checking local constraints is exactly the same, up to the labeling of variables. So, given the index of a 3CNF clause of $f(x)$, we need the circuit $C(x)$ to:
- figure which tableau cell it corresponds to
- if it corresponds to the first $|x|$ entries of the first row or the first entry of the last row of the tableau, output the clause
- if it corresponds to any other cell, we're dealing with the same constant-size 3CNF, and we only need to compute the variable labels for it, which can be done based only on the index of the tableau cell
Steps 1 and 3 are basically arithmetic based on the index of the clause of $f(x)$ and the index of the tableau cell it corresponds to. Both these indexes can be written in $O(p(|x|))$ bits and steps 1 and 3 therefore can be done in time polynomial in $|x|$. Since any function computable in polynomial time can be computed using a polynomial size circuit, we have poly size circuits for 1 and 3. For step 2 we need to just hard-wire $O(|x|)$ 3CNF terms into the circuit. Put all these together, and we're done.
