Finish fixes to repl proof