get stuck in sequence (and while) case. IH is no good!

(forall k, pick_spH (k ++ kH) = pick_spL (rev kL ++ snd (fst (dtransform_stmt_trace eH (rev k, sH, used_after)))))

^this part is too strong.  not preserved when passing to first subcommand of
seq.  we don't want equality for all k; we just want equality for short
enough k.  but this would be obnoxious to work with, I think.

if I had the continuation here, then putting that extra degree of freedom
in there allows it to be true for all k!  I think putting the continuation
back would be much less pain, in the end.  the short-circuiting thing in
writing the function is really annoying, anyway

There are a couple dimensions along which these trace-transformation
functions proofs can vary: we can either have the deterministic stackalloc
or not, and I we can either have the function written in CPS or not.  Before
this, I had explored three points in this space, and they all worked out
fine.  Here I explored the fourth, deterministic stackalloc + not-CPS, and
it did not work as well.

compiler/src/compiler/DeadCodeElim.v

@@ -293,19 +293,22 @@ Section WithArguments1.
            reflexivity.
         -- unfold compile_post. intros. fwd. solve_compile_post.
            rewrite H2p6. reflexivity.
-    - intros.
+    - admit. (*intros.
       cbn - [live].
       rename IHexec into IH1.
       rename H6 into IH12.
       rename H4 into IH2.
       cbn - [live] in IH12.
-      eapply @exec.loop with (mid2 := compile_post mc mcL (live (SLoop body1 cond body2) used_after) mid2).
+      eapply exec.loop_cps. Check exec.loop_cps. Check IH1.
+      eapply exec.weaken.
       { eapply IH1.
-        eapply agree_on_subset.
-        - let Heq := fresh in
-          specialize (live_while body1 cond body2 used_after) as Heq; cbn zeta in Heq.
-          eapply H4.
-        - eapply H7.
+        - eapply agree_on_subset.
+          + let Heq := fresh in
+            specialize (live_while body1 cond body2 used_after) as Heq; cbn zeta in Heq.
+            eapply H4.
+          + eapply H7.
+        - intros. rewrite H8. rewrite dfix_step. cbn [dtransform_stmt_trace_body].
+          simpl.
       }
       { intros.
         unfold compile_post in *.
@@ -359,10 +362,15 @@ Section WithArguments1.
         - eapply H4.
         - cbv beta. intros * (?&?&?&?&?).
           eexists. mcsolve.
-      }
+      }*)
     - intros.
       eapply @exec.seq.
-      + eapply IHexec. eassumption.
+      + eapply IHexec; [eassumption|].
+        intros. rewrite H4. rewrite dfix_step. simpl.
+        (*this would work either with continuation or with nondeterministic
+          stackalloc.  only fails with both (1) no continuation and (2)
+          deterministic stackalloc...*)
+        rewrite 
       + unfold compile_post. intros. fwd.
         eapply @exec.weaken.
         * eapply H2.