Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line. Use ALT-(right-arrow) to go to the cursor. You can inside your browser and . Finally, you can your working copy of the file, e.g., for sending it to teachers.

### Exercise 5

The next exercise consists in proving an alternative induction scheme on type list, whose base case is the last element in the list.

For this purpose, we first define a concatenation operation between lists and prove a few lemmas about it.

The 'rcons' operation is provided by the underlying library, and appends its last argument to the end of its first, which is a list.

The exercise is self-contained : you should not use results that you did not prove yourself.

### Exercise 10.

#### Prove lemma last_ind using first the intermediate lemma hcat,

and then by induction. Hint: use the lemmas you have proved so far on function cat.