start on compile_decs_thm

but want to remove the optimisation for a single dec - the proof is more
uniform if the implementation unwraps the tuple, then immediately
re-wraps it to pop the exception, then unwraps it again. (in the general
case the wrap is of more stuff than just the tuple that was just
unwrapped.)

could prove as a bytecode optimisation that an unwrap followed by a wrap
is a no-op, then compile_decs wouldn't have to special-case. (or could
then define the optimised compile_decs and show it produces equivalent
bytecode.)
remove optimisation from compile_decs{,_wrap}