This talk proved two theorems: Substitution theorem and characterization of persistently strongly normalizing terms. Substitution theorem is for usual lambda calculus (untyped lambda calculus with beta-reduction). We say a term M is strongly normalizing if it terminates with any reduction strategy. A simple instance of Substitution theorem is that for any term M, MXYZ is strongly normalizing for any strongly normalizing terms X,Y,Z if MXXX is strongly normalizing for any strongly normalizing term X. This means that in order to prove termination of a 3-place function f(x,y,z) in a functional programming language, it is sufficient to show termination of the function call f(x,x,x). A term M is called persistently strongly normalizing if MX_1 … X_n is strongly normalizing for any n and any strongly normalizing terms X_1, …, X_n. A type theoretic characterization of these terms was a long-standing open question. This talk solved this problem by using Substitution theorem. This is a joint work with Mariangiola Dezani-Ciancaglini (Torino University).