in [@deGr], is an extension of Parigot’s $\l\m$-calculus. It is the computational counterpart of classical natural deduction with $\f$, $\et$ and $\ou$. Three notions of conversions are necessary in order to have the sub-formula property : logical, classical and permutative conversions.

The proofs of the strong normalization of the cut-elimination procedure for the full classical logic are quite recent and three kinds of proofs are given in the literature.

[*Proofs by CPS-translation*]{}. In [@deGr] de Groote also gave a proof of the strong normalization of the typed $\l\m^{\f\et\ou}$-calculus using a CPS-translation into the simply typed $\l$-calculus i.e. the implicative intuitionistic logic but his proof contains an error as Matthes pointed out in [@Mat1]. Nakazawa and Tatsuta corrected de Groote’s proof in [@NaTa] by using the notion of augmentations.

[*Syntactical proofs*]{}. We gave in [@DaNo2] a direct and syntactical proof of strong norma-lization. The proof is based on a substitution lemma which stipulates that replacing in a strongly normalizable deduction an hypothesis by another strongly normali-zable deduction gives a strongly normalizable deduction. The proof uses a technical lemma concerning commutative reductions. But, though the idea of the proof of this lemma (as given in [@DaNo2]) works, it is not complete and 