another case of compile_val
change compilation of Seq

make it pop the first value off the stack
non-error cases of Seq case of compile_val

Seq turns out to be a reasonably complex new language form, at least in
the context of this terribly complicated proof... luckily most of the
cases that aren't new seem to go through with just tweaks, so I only
have to prove Seq and the global env manipulations.