Further progress on simple handlers for the translator.

It's a really intricate and annoying proof with some cheats in, but I
think the last theorem eval_decs'_to_eval_decs_simple_pat is probably
true.