In class we derived this typing using and informal version of algorithm .Question: Does (lazy) respect typing? ie
The subject reduction theorem shows that it does.