  In the late 1960s, strong normalization became an issue:  Prawitz, using previous work of William Tait and Jean-Yves Girard,  proved in 1971 that non-normalities in a derivation can be converted  in any order, with a terminating normalization process and a unique  normal derivation as a result. Gentzen seems not to have noticed the  latter, but seems to have thought rather the contrary, by the failure of this property for the elimination of cuts in sequent calculus.