A general reducibility method for proving reduction properties of the simply typed lambda calculus is presented and sufficient conditions for its application are derived.