> So S might lead to intermediate terms which are not typeable, but my > question is, as I am going from a typed to another typed term, are these > intermediate untypeable terms somehow superfluous? Why do you think beta/eta reduction might lead to untypeable terms when the starting term is typed? Can you give an example? Immanuel