move a lemma from replCorrect back to compilerProofs