  A simple, but very important corollary of normalization is the following: Every closed derivation in intuitionistic logic can be reduced to a derivation using an introduction rule in the last step. We also say that intuitionistic natural deduction satisfies the “introduction form property”. In proof-theoretic semantics this result figures prominently under the heading “fundamental assumption” (Dummett, 1991, p. 254). The “fundamental assumption” is a typical example of a philosophical re-interpretation of a technical proof-theoretic result.