  In this article we show how any formula A with a proof in minimal
implicational logic that is super-polynomially sized has a polynomially-sized
proof in classical implicational propositional logic . This fact provides an
argument in favor that any classical propositional tautology has short proofs,
i.e., NP=CoNP.
