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?