Normalization. PCF Saturated sets Simultaneous substitution Strong normalization proof Extensions (pairs, sums, fix)