+interpretation "append" 'append l1 l2 = (append ? l1 l2).
+
+(* As usual, the function is executable. For instance, (append A nil l) reduces to
+l, as shown by the following example: *)
+
+example nil_append: ∀A.∀l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A. \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 l \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+#A #l normalize // qed.
+
+(* Proving that l @ [] = l is just a bit more complex. The situation is exactly the
+same as for the addition operation of the previous chapter: since append is defined
+by recutsion over the first argument, the computation of l @ [] is stuck, and we must
+proceed by induction on l *)
+
+lemma append_nil: ∀A.∀l:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.l \ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6 \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6] \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 l.
+#A #l (elim l) normalize // qed.
+
+(* similarly, we can define the two functions head and tail. We should decide what to do in
+case the input list is empty. For tl, it is natural to return the empty list; for hd, we take
+in input a default element d of type A to return in this case. *)
+
+definition head ≝ λA.λl: \ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.λd:A.