[FOM] Proof-theoretic proof of NP=PSPACE?

[Alasdair Urquhart]

I think there must be an error in this proof somewhere.
Pavel Hrubes proved an exponential lower bound on
proofs in the intuitionistic propositional calculus
(Annals of Pure and Applied Logic, Volume 146 (2007),
pp. 72-90.  There is an efficient translation from
intuitionistic logic into minimal logic, so the
claimed result contradicts the theorem of Hrubes.