3. For this chapter, I would emphasize that all its semantic definitions are very natural and very simple, in the strong sense that there really isn't anything else you could write. The only exception to this is the use of EStore instead of just Store, which seems artificial at this point, because it is really not needed for the constructions in Chapter 3; in fact, Proposition 27 can be seen as proving that EStore isn't needed here. However, as the chapter repeatedly emphasizes, EStore becomes necessary when programs can have while loops, because these may not terminate; therefore we may as well write the definitions in the way we will eventually need them anyway.

3.3 The proof of Proposition 27 is not difficult, and the result is intuitively obvious, although it is a bit technical to give a precise definition for "structural induction" and to justify it; the formulation of program terminatation in Proposition 27 is also a bit technical, and a little thought is required to understand it.

Regarding the proof of Proposition 27 for the case of the conditional as requested in Exercise 14, note that you should first prove a lemma, that expressions of sort Tst always return either true or else false; this can be done using structural induction in the same style as in the main proof.