thoughts towards proving evaluate_dec_closed

looks like some of the work can be copied (and tweaked) from the old
semanticsExtraTheory