Although similar to a previously unanswered question, my query focuses on a different aspect of normalization. I'm trying to adjust the proof of strong normalization of STLC, given in Jeremy Avigad's book, to prove it in locally nameless representation. I'm referencing Arthur Chargueraud's paper for the locally nameless representation.. Until a lemma about lambda terms, everything fit well. But I couldn't figure out the following lemma.
Lemma 13.2.8. Suppose that whenever $s$ is strongly computable, $t[s/x]$ is strongly computable. Then $\lambda x. t$ is strongly computable.
After some steps, proof involves a case analysis on the reducts of the application term $(\lambda x. t) s$. One possibility is $(\lambda x. t')s$ where $t \rightarrow_1 t'$, and inductive hypothesis gives the result. However, in locally nameless representation, the situation is different. If the reduction happens on first (lambda) part, it is of the form $\forall x \notin L, t^x \rightarrow_1 t'^x$ where $L$ is a finite set. This is the definition (BETA-ABS) in Section 4.5 in the chapter. Here, $t^x$ denotes the variable opening (Section 3.1). About variable opening, we know from the paper:
Variable opening turns some bound variables into free variables. It is used to investigate the body of an abstraction.
Also, when a term $t$ is locally closed (Section 3.3), variable opening fixes the term, namely $t^x=t$.
In the reduction step above, I know that $t$ is locally closed, so $t^x \rightarrow_1 t'^x$ becomes $t \rightarrow_1 t'^x$. However, I'm not able to say it for $t'$ sure. That's why I'm not able to work with the induction like in the book. Therefore, I believe the lemma should be adapted to the locally nameless style. There is a relationship between substition and variable opening, but it's hard to explain for me. I have a vague sense.
How can we adjust the lemma (if we can) to obtain a criteria for strongly computable lambda terms?
EDIT: Following the idea in the comments and using the idea in the paper, I stated and proved the criteria for lambda terms as follows:
Suppose that whenever $s$ is strongly computable, $t^x[s/x]$ is strongly computable. Then $\lambda t$ is strongly computable.
As a corollary, I also have:
Suppose that whenever $u$ is strongly computable, $t^u$ is strongly computable. Then $\lambda t$ is strongly computable.
