work on compile_decs_thm last cheat

but mostly work on proving things about PERM... but now I think I just
need to change the implementation to do more REVERSE-ing so it matches
the semantics even closer... I'm not sure exactly how they differ at the
moment, but something is wrong in the order of some list somewhere.
prove last cheat in compile_decs_thm, change statement slightly

write a custom function to compute what the renv would look like after
doing a series of declarations (the issue is that it's not a simple MAP
over all the new bindings: the bindings for each declaration get added
in order in a single chunk, and the declarations get processed in order,
but adding is consing, so there are two layers of reversing going on).

hopefully this will be ok for compile_decs_wrap's theorem to deal
with...