prove evaluate_closed
prove evaluate_dec_closed

use it to prove a cheat in compile_top_thm