improve definition of closed_context, and simplify proofs accordingly
prove cheats in evaluate_top_closed_context
fix repl_fun to keep some of the inferencer state in the error case

and prove some of the missing invariant-preservation case in
repl_correct_lem. I think the implementation may still be broken though,
because it probably throws away the constructor and module environments
at the compiler level in the case of an error.