finish Dletrec case of compile_dec_val

Dtype case remains.

(Also there's the cheat about equivalent environments in the proof of
compile_fake_exp_val, and the cheats for exceptions in compile_val.)