Hello,
Just to tell you that a correction of exercise 16 (Natural Operationnal Semantics) is available online:
https://im2ag-moodle.univ-grenoble-alpes.fr/mod/resource/view.php?id=38704
This rather complete exercise helps to better understand the inductive proof techniques used at the beginning of this semester.
Have a nice end of week,
L. Mounier