Define

check n k w = (#w = n) -> (k w), wrong

Claim:  for k strict,

E*[e*] r k = E*[e*] r (check #e* k)

Proof:

E*[] r k = k nil

E*[] r (check 0 k) = (#nil = 0 -> k nil, wrong)
                   = k nil

E*[e e*] r k = E[e] r (\v. E*[e*] r (\w. k (cons v w)))

             = E[e] r (\v. E*[e*] r (\w. #w = #e* -> (k (cons v w)), wrong)
							[IH] 
             = E[e] r (\v. E*[e*] r (\w. (#(cons v w) = #e* + 1)
					 -> (k (cons v w)), wrong)

			[since #w = #e* iff #(cons v w) = #(e e*) = #e* + 1]

             = E*[e e*] r (check #(e e*) k)

Now with this lemma, we can do the rest of the proof.  I'm going to omit the
symbol table argument to the compiler.  Also I'll not worry about checking
that all the continuation in question are strict (that should be easy, and I'm
not sure it's necessary).  Also I'll use  M -> N as an abbreviation for (M ->
N, wrong).

We have:

E*[] r k = k nil
E*[e e*] r k = E[e] r (\v. E*[e*] r (\w. k (cons v w)))

C*[] pi = pi
C*[e e*] pi = C[e] (C*[e*] pi)

Induction Hypotheses:

(C[e] pi) r z = E[e] r (\v. pi r (cons v z))
(C*[e*] pi) r z = E*[e*] r (\w. pi r (apprev w z))

where apprev is defined by

(apprev nil z) = z
(apprev (cons v w) z) = (apprev w (cons v z))

The cases for C* go through as usual.  The trouble shows up when we use C* in
C.  Let's consider an n-ary operation:

E[op e*] r k = E*[e*] r (\w. k (do-op w))

This should be compiled as:

C[op e*] pi = C*[e*](op-ins #e* pi)

Let's do the induction step.  We assume (C*[e*] pi) r z = E*[e*] r (\w. pi r
(apprev w z)), and we want to show

(C[op e*] pi) r z = E[op e*] r (\v. pi r (cons v z))

Expanding the LHS:

(C[op e*] pi) r z 

= C*[e*](op-ins #e* pi) r z

= E*[e*] r (\w. op-ins #e* pi r (apprev w z))

= E*[e*] r (\w. #w = #e* -> op-ins #e* pi r (apprev w z))

Expanding the RHS:

E[op e*] r (\v. pi r (cons v z))

= E*[e*] r (\w. pi r (cons (do-op w) z))

= E*[e*] r (\w. #w = #e* -> pi r (cons (do-op w) z))

So what's left is a reasonable-looking lemma:

#w = #e* -> op-ins #e* pi r (apprev w z) =  pi r (cons (do-op w) z))

[Now, we've cheated here, in that -> now means something different from what
it meant before.  But let's go on].

If we define op-ins by
 
op-ins n pi r z = op-ins-loop n pi r nil z

op-ins-loop 0   pi r w z = pi r (cons (do-op w) z)
op-ins-loop n+1 pi r w z = op-ins-loop n pi r (cons (car z) w) (cdr z)

then all this should work; we need to define a suitable induction hypothesis
about op-ins-loop, but that should be routine.