The proof of the weakening lemma (lemma 12) is incorrect. At the end
of the proof, the argument "By iterated application of the initial
induction hypothesis" used to reduce the statement
(v|E)sigma'[x<-v']sigma'' SN to the statement
(v|E[x<-v'])sigma'sigma'' SN is wrong. Indeed, it would require a
stronger induction hypothesis for which x:A is not necessarily the
last declaration in the context.
At the time being, we do not have any simple fix. A priori, we should
renounce to a reducibility-based proof argument and use rather a
purely combinatory proof of "(v|E[x<-v'])sigma'sigma'' SN ->
(v|E)sigma'[x<-v']sigma'' SN". That's just another place in the proof
that shows that the reducibility method do not help for dealing with
explicit substitutions which at the end remain of a purely
combinatorial nature.
However, the weakening lemma is still considered true and the whole
structure of the proof, including the specific notion of reducibility
sets we considered, is a priori not affected and still relevant.
I thank Pierre-Louis Curien for having pointed out the problem.
Notice that a more general proof of strong normalisation of the
simply-typed lambda-bar-mu-mu-tilde-calculus for a non deterministic
reduction system has been given by Emmanuel Polonovski in "Strong
normalization of lambda-bar-mu-mu-tilde-calculus with explicit
substitutions", Foundations of Software Science and Computation
Structures (FOSSACS 2004), LNCS volume 2987, p. 423-437, Springer,
2004.