A bounded translation of intuitionistic propositional logic into basic propositional logic