To play this document inside your browser use ALT-N and ALT-P.

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

---

Cheat sheet available at https://www-sop.inria.fr/teams/marelle/types18/cheatsheet.pdf

Exercise 1:

• use no lemma to prove the following statement

Exercise 2:

• look up what ==> is and prove that as you like

Exercise 3:

• what is (+) ?
• prove this using move and rewrite

Exercise 4:

• prove this satement by induction

Exercise 5:

• look up the definition of iter (note there is an accumulator varying during recursion)
• prove the following statement by induction

---