Herbrand's Theorem for Calculi of Sequents LK and LJ

We sketch a simple proof of Herbrand's theorem for Gentzen's calculi of sequents LK and LJ in the general case, without restrictions to sequents containing only prenex formulas. In the case of classical logic LK, the statement of the theorem is that for any sequent S of LK, S is derivable in first order LK if and only if for some p the Herbrand expansion E_p(S) is provable in the propositional part of LK. In the case of intuitionistic logic LJ, a sequent S is derivable in first order LJ if and only if for some p the Herbrand expansion E_p(S) is provable in the propositional part of LJ with an "adequate" proof, where a proof of E_p(S) is adequate if it satisfies certain conditions on permutability of inferences given in Kleene 1952.