diff --git a/CHANGELOG.md b/CHANGELOG.md
index 80799303dfbe12b3049ec2248f2e482babcd9091..ad6707e006c9d85b94a88475dbc7d7dbe95ffda9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -68,6 +68,11 @@ API-breaking change is listed.
   + Generalize lemmas `partial_alter_merge`, `partial_alter_merge_l`, and
     `partial_alter_merge_r`.
   + Drop unused `merge_assoc'` instance.
+- Improvements to `head` and `tail` functions for lists:
+  + Define `head` as notation that prints (Coq defines it as `parsing only`)
+    similar to `tail`.
+  + Declare `tail` as `simpl nomatch`.
+  + Add lemmas about `head` and `tail`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/tests/list.ref b/tests/list.ref
new file mode 100644
index 0000000000000000000000000000000000000000..ac5cc48d46a5a1538950047afc8d239e7b20583d
--- /dev/null
+++ b/tests/list.ref
@@ -0,0 +1,22 @@
+1 goal
+  
+  ============================
+  None = None
+1 goal
+  
+  ============================
+  Some 10 = Some 10
+1 goal
+  
+  ============================
+  Some 11 = Some 11
+1 goal
+  
+  l : list nat
+  ============================
+  last (11 :: l) = last (11 :: l)
+1 goal
+  
+  l : list nat
+  ============================
+  last (10 :: l) = last (10 :: l)
diff --git a/tests/list.v b/tests/list.v
new file mode 100644
index 0000000000000000000000000000000000000000..dd1d58fbb880ee1d2a14263a896c317001e3df13
--- /dev/null
+++ b/tests/list.v
@@ -0,0 +1,17 @@
+From stdpp Require Import list.
+
+Lemma last_simpl_test_nil : last [] =@{option nat} None.
+Proof. simpl. Show. done. Qed.
+
+Lemma last_simpl_test_singleton : last [10] = Some 10.
+Proof. simpl. Show. done. Qed.
+
+Lemma last_simpl_test_double : last [10; 11] = Some 11.
+Proof. simpl. Show. done. Qed.
+
+Lemma last_simpl_test_cons_cons l : last (10 :: 11 :: l) = last (11 :: l).
+Proof. simpl. Show. done. Qed.
+
+(* The following should not [simpl] and result in a [match]. *)
+Lemma last_simpl_test_cons l : last (10 :: l) = last (10 :: l).
+Proof. simpl. Show. done. Qed.
diff --git a/theories/list.v b/theories/list.v
index 63a3ce6ad2fb910c7bb03dd298f4cd39fac0b1e0..ef88844b679031164aa2d8bb6b95aea23ae95b43 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -15,12 +15,18 @@ Global Instance: Params (@length) 1 := {}.
 Global Instance: Params (@cons) 1 := {}.
 Global Instance: Params (@app) 1 := {}.
 
+(** [head] and [tail] are defined as [parsing only] for [hd_error] and [tl] in
+the Coq standard library. We redefine these notations to make sure they also
+pretty print properly. *)
+Notation head := hd_error.
 Notation tail := tl.
+
 Notation take := firstn.
 Notation drop := skipn.
 
 Global Arguments head {_} _ : assert.
 Global Arguments tail {_} _ : assert.
+
 Global Arguments take {_} !_ !_ / : assert.
 Global Arguments drop {_} !_ !_ / : assert.
 
@@ -168,6 +174,7 @@ if the list [l] is empty. *)
 Fixpoint last {A} (l : list A) : option A :=
   match l with [] => None | [x] => Some x | _ :: l => last l end.
 Global Instance: Params (@last) 1 := {}.
+Global Arguments last : simpl nomatch.
 
 (** The function [resize n y l] takes the first [n] elements of [l] in case
 [length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
@@ -1084,10 +1091,56 @@ Proof.
 Qed.
 
 (** ** Properties of the [last] function *)
+Lemma last_nil : last [] =@{option A} None.
+Proof. done. Qed.
+Lemma last_singleton x : last [x] = Some x.
+Proof. done. Qed.
+Lemma last_cons_cons x1 x2 l : last (x1 :: x2 :: l) = last (x2 :: l).
+Proof. done. Qed.
+
+Lemma last_None l : last l = None ↔ l = [].
+Proof.
+  split; [|by intros ->].
+  induction l as [|x1 [|x2 l] IH]; naive_solver.
+Qed.
+Lemma last_is_Some l : is_Some (last l) ↔ l ≠ [].
+Proof. rewrite <-not_eq_None_Some, last_None. naive_solver. Qed.
+
+Lemma last_cons x l :
+  last (x :: l) = match last l with Some y => Some y | None => Some x end.
+Proof.
+  destruct l as [|x' l]; simpl; [done|].
+  destruct (last (x' :: l)) eqn:Hlast; [done|].
+  by apply last_None in Hlast.
+Qed.
 Lemma last_snoc x l : last (l ++ [x]) = Some x.
 Proof. induction l as [|? []]; simpl; auto. Qed.
+Lemma last_lookup l : last l = l !! pred (length l).
+Proof. by induction l as [| ?[]]. Qed.
+
 Lemma last_reverse l : last (reverse l) = head l.
-Proof. by destruct l as [|x l]; rewrite ?reverse_cons, ?last_snoc. Qed.
+Proof. destruct l as [|x l]; simpl; by rewrite ?reverse_cons, ?last_snoc. Qed.
+
+(** ** Properties of the [head] function *)
+Lemma head_nil : head [] =@{option A} None.
+Proof. done. Qed.
+Lemma head_cons x l : head (x :: l) = Some x.
+Proof. done. Qed.
+
+Lemma head_None l : head l = None ↔ l = [].
+Proof. split; [|by intros ->]. by destruct l. Qed.
+Lemma head_is_Some l : is_Some (head l) ↔ l ≠ [].
+Proof. rewrite <-not_eq_None_Some, head_None. naive_solver. Qed.
+
+Lemma head_snoc x l :
+  head (l ++ [x]) = match head l with Some y => Some y | None => Some x end.
+Proof. by destruct l. Qed.
+Lemma head_snoc_snoc x1 x2 l :
+  head (l ++ [x1; x2]) = head (l ++ [x1]).
+Proof. by destruct l. Qed.
+Lemma head_lookup l : head l = l !! 0.
+Proof. by destruct l. Qed.
+
 Lemma head_reverse l : head (reverse l) = last l.
 Proof. by rewrite <-last_reverse, reverse_involutive. Qed.