Program reductions are used widely to simplify reasoning about the correctness of concurrent and distributed programs. Different reduction techniques are often tailored towards specific classes of programs, for example message passing vs shared memory. In this paper, we propose a general approach to proof simplification of concurrent programs based on exploring generic classes of reductions. We introduce two classes of sound program reductions, study their theoretical properties, show how they can be effectively used in algorithmic verification, and demonstrate that they are very effective in producing proofs of a diverse class of programs without targeting specific syntactic properties of these programs. We modify the classic counterexample-guided refinement loop of automated program verification so that, in addition to proof search, it also searches for a program reduction that admits a substantially simpler proof of correctness compared to the original program. This methodology, hence, succeeds in automatically generating proofs for programs whose full proofs are theoretically outside the reach of current automated verification technology.