Monotone simulations of nonmonotone proofs

We show that an LK proof of size m of a monotone sequent (a sequent that contains only formulas in the basis ∧, V) can be turned into a proof containing only monotone formulas of size m^{O(log m)} and with the number of proof lines polynomial in m. Also we show that some interesting special cases, namely the functional and the onto versions of PHP and a version of the matching principle, have polynomial size monotone proofs