In this paper we give a proof of the strong normalisation theorem for intuitionistic type theory. Cut-elimination is an immediate consequence of it. The basic ideas of our proof are the use of wellfoundedness predicates, originally due to J. Y. Girard [1] and a mapping from the derivations in type theory into a type-free
-calculus, which we learned in a lecture, given by W. Tait at Munich 1972.