Normalization, Cut-Elimination & the Theory of Proofs door A.M. Ungar