prove all but invariant preservation of repl_correct_lem

closedness cheats are also still there