La preuve du lemme d'affaiblissment (lemme 12) est trouée. Vers la fin de la preuve, pour montrer que (v|E)sigma'[x<-v']sigma'' est SN, l'argument "By iterated application of the initial induction hypothesis" pour se ramener au cas (v|E[x<-v'])sigma'sigma'' SN est incorrect car il nécessite une hypothèse d'induction où x:A n'est pas forcément la dernière déclaration du contexte. À l'heure actuelle, nous n'avons pas de réparation simple de la preuve. A priori, il faudrait renoncer à raisonner sur la réductibilité et se rabattre sur une preuve combinatoire de "(v|E[x<-v'])sigma'sigma'' SN -> (v|E)sigma'[x<-v']sigma'' SN", limitant d'autant l'intérêt de la notion réductibilité pour gérer ce qu'il convient donc d'appeler la combinatoire des substitutions explicites. Malgré cela, nous ne pensons pas que l'énoncé lui-même du lemme d'affaiblissement soit en cause. En particulier, la structure globale de la preuve complète de SN ainsi que la notion particulière d'ensembles réductibles que nous avons considérée restent a priori pertinentes. Merci à Pierre-Louis Curien d'avoir remarqué ce problème. Précisons par ailleurs qu'une preuve plus générale de normalisation forte du calcul lambda-bar-mu-mu-tilde simplement typé pour un système de réduction non-déterministe a été réalisée par Emmanuel Polonovski dans "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.