fix proof of evaluate_top_closed_context

this and other theorems in replCorrect should probably be moved elsewhere...