Exercises for the third day

[Yves]

Hard exercise:

Copy syntax.v, little.v, and axiom.v into syntax2.v little2.v and
axiom2.v

remove all the stuff related to sos from little2.v

Add a conditional statement to the syntax, add its description in
exec,
also add its description in the axiomatic semantics. Prove the whole
thing
sound.

This can take a few hours (or days).

Easy exercises

Use axiomatic semantics to redo the proof of ex2 and ex4 (take
inspiration in
the file example2.v)