apply H3; apply le_S_S_to_le; apply H4]
qed.
+definition last ≝
+ λT:Type.λd.λl:list T. \nth l d (pred (\len l)).
+
+notation > "\last" non associative with precedence 90 for @{'last}.
+notation < "\last d l" non associative with precedence 70 for @{'last2 $d $l}.
+interpretation "list last" 'last = (last _).
+interpretation "list last applied" 'last2 d l = (last _ d l).
+
+definition head ≝
+ λT:Type.λd.λl:list T.\nth l d O.
+
+notation > "\hd" non associative with precedence 90 for @{'hd}.
+notation < "\hd d l" non associative with precedence 70 for @{'hd2 $d $l}.
+interpretation "list head" 'hd = (head _).
+interpretation "list head applied" 'hd2 d l = (head _ d l).
+