A Proof of Strong Normalization of F_2, F_omega and Beyond - David A. McAllester; J. Kucan; D. F. Otth (Inf. Comput., 1995)