finish divergence proofs in repl_correct_lem

the only (inherited) cheats should be for modules and closedness.