 (Note: The notion of suitable “substitution” is much more complicated for logic of higher types than it is for first order logic. In part this is because of the application to an argument of lambda expressions for a propositional function, e.g., \([\lambda x \phi (x)] (\nu)\) where \(\nu\) may be a complex term involving variables and quantifiers in other lambda expressions.)