Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo