Closures break induction in correctness proof of interpreter

I'm trying to prove the correctness of an interpreter for a simple extension of untyped lambda-calculus with De Bruijn indices. The interpreter is bounded, i.e. in order to ensure its finiteness it has an additional parameter $n \in \mathbb N$ that decreases with each recursive call. The function returns $\bot$ when $n = 0$.

This is the signature of the interpreter: $\mathcal E : (\mathbb N, Env, E) \to (Val \cup \{\bot\})$

Where $Env$ is the set of environments, represented as lists of values accessed with De Bruijn indices, $E$ is the set of expressions and $Val$ is the set of values:

$$ \begin{aligned}
E &::= \lambda E \mid EE \mid A \mid B \mid \texttt{if } E \texttt{ then } E \texttt{ else } E \mid x \in Var \mid V\\
A &::= \textit{integer operations...} \\
B &::= \textit{boolean operations...} \\
V &::= \texttt{True} \mid \texttt{False} \mid c \in \mathbb Z \mid \texttt{Closure} (\rho, E)
\end{aligned} $$
Soundness theorem

$$\forall e, \rho, n, v . \mathcal E (n, \rho, e) = v \implies \langle e, \rho \rangle \to^* v$$

I.e.: If $e$ evaluates to $v$ under the initial environment $\rho$ and in a finite number of steps, then there exists a finite proof that it does, which uses the rules of the small-step semantics I describe in the "appendix" of this post.
Proof Attempt Sketch

I tried to prove the theorem by induction on $e$.
Base Cases

The base cases are lambdas, values and variables. I managed to prove these cases with ease.

• Lambdas: Let $e = \lambda e'$. First off, the case in which $n = 0$ can be eliminated, since it makes the premise of the theorem false (ex falso...). If $n = Sm$, by the definition of the interpreter we get that the value $v$ must be $\texttt{Closure}(\rho, e')$. The case can be shown to work by applying the LAMBDA rule, some properties of the star closure and the VALUE rule.

• Values: trivial.

• Variables: Use rule VAR-KO to eliminate the case in which the variable is not in the environment. Then, it's a matter of appl

You must strengthen the theorem to be proved by induction. In the $e_1e_2$ case, the current induction hypothesis just tells you that $e_1$ reduces to a closure, but not anything more about how the enclosed expression reduces. Another hint that something is missing is that in the $\lambda x . e$ case (and the closure case which is hidden under "values"), you don't make use of the induction hypothesis on $e$, which is precisely about how $e$ reduces.

You will have more luck with a proof by induction on a recursive property like the following:

$P(e) = ``\forall n \rho v,\; \mathcal{E}(n,\rho,e) = v \implies (\rho,e) \to^\star v \wedge (\forall \rho' e',\; v = \mathbf{Closure}(\rho',e') \implies P(e'))"$

This creates new problems that you will have to figure out (Now it's too strong for the case of variables, how to weaken it a bit? Is this recursive property even well-defined? (if not, how to make it so?)). Hopefully this gets the ball rolling for you.

StackExchange Computer Science Q#165370, answer score: 3