update some free_vars definitions
update proof of evaluate_closed