Please read Chapter 9 in the textbook.
In class, we discussed several dubious type rules. In particular, we
discussed something similar the following system:
Suppose we try to prove progress and preservation (for closed terms)
with this ``type system.''
Can we do it? Explain! Give concrete examples.
If we changed the rules to
Can we prove progress and preservation? Discuss!
Read Exercise 9.2.3 and prove that if
then we have a contradiction.
Do the proof of preservation (Theorem 9.3.9).
You will need to use the substitution lemma (Lemma 9.3.8).