Is there a simpler proof of Beigel and Tarui's transformaion of ACC0 circuits

Question

Beigel and Tarui's transformation of $\mathsf{ACC}^0$ circuits to depth 2 circuits with a polylog symmetric function on top is one of important results in the circuit complexity. For example, the recent breakthrough separation between $\mathsf{NEXP}$ and $\mathsf{ACC}^0$ by Ryan Williams uses this transformation to design a fast $\mathsf{ACC}^0$-CircuitSAT algorithm.

I think the proof in their paper is a little complicated and too technical for me. Is there a simpler proof of their result?

Answer 1

This result is presented in the Web Addendum of Arora-Barak, which can be found here.