+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).
+