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.