more work on compile_dec_thm
add another invariant to env_rs

that "" is actually bound to tuple_cn
finish compile_dec_thm

require a tweak to the implementation - had forgotten about the
block_tag
wip on a lemma about compile_decs

should probably just go straight to trying to state the main theorem
aobut it though.