Normalization without reducibility

In Gallier (Ann. Pure Appl. Logic 91 (1998) 231-270), general results (due to Coppo and Dezani, Arch. Math. Logic 19 (1978) 139-156; Coppo et al., Z. Math. Log. Grund. Math. 27 (1981) 45-58) relating properties of pure lambda terms and their typability in some systems with conjunctive types D Omega and D are proved in a uniform way by using the reducibility method. This pa per gives a very short proof of the same results (actually, one of them is a bit stronger) using purely arithmetical methods. (C) 2001 Elsevier Scienc e B.V. All rights reserved.