diff --git a/CHANGELOG.md b/CHANGELOG.md
index 222e13e8e7a74e237dfea3efe10828f2ed34a460..ca42db3673b1fcabd2763148e0e3f4a87576d714 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,8 @@ API-breaking change is listed.
 
 - Add `disj_union_list` and associated lemmas for `gmultiset`. (by Marijn van Wezel)
 - Add lemma `lookup_total_fmap`.
+- Add lemmas about `last` and `head`: `last_app_Some`, `last_app_None`,
+  `head_app_Some`, `head_app_None` and `head_app`. (by Marijn van Wezel)
 
 ## std++ 1.11.0 (2024-10-30)
 
diff --git a/stdpp/list.v b/stdpp/list.v
index 1b4c3ecd08422b93acf707f108ffda7763a0a440..64096df6e32adc11d3d4b38cbe4830795ad8b867 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -1220,6 +1220,12 @@ Proof.
   - by rewrite (right_id_L _ (++)).
   - by rewrite (assoc_L (++)), !last_snoc.
 Qed.
+Lemma last_app_Some l1 l2 x :
+  last (l1 ++ l2) = Some x ↔ last l2 = Some x ∨ last l2 = None ∧ last l1 = Some x.
+Proof. rewrite last_app. destruct (last l2); naive_solver. Qed.
+Lemma last_app_None l1 l2 :
+  last (l1 ++ l2) = None ↔ last l1 = None ∧ last l2 = None.
+Proof. rewrite last_app. destruct (last l2); naive_solver. Qed.
 Lemma last_cons x l :
   last (x :: l) = match last l with Some y => Some y | None => Some x end.
 Proof. by apply (last_app [x]). Qed.
@@ -1259,6 +1265,15 @@ Proof. by destruct l. Qed.
 Lemma head_lookup l : head l = l !! 0.
 Proof. by destruct l. Qed.
 
+Lemma head_app l1 l2 :
+  head (l1 ++ l2) = match head l1 with Some y => Some y | None => head l2 end.
+Proof. by destruct l1. Qed.
+Lemma head_app_Some l1 l2 x :
+  head (l1 ++ l2) = Some x ↔ head l1 = Some x ∨ head l1 = None ∧ head l2 = Some x.
+Proof. rewrite head_app. destruct (head l1); naive_solver. Qed.
+Lemma head_app_None l1 l2 :
+  head (l1 ++ l2) = None ↔ head l1 = None ∧ head l2 = None.
+Proof. rewrite head_app. destruct (head l1); naive_solver. Qed.
 Lemma head_reverse l : head (reverse l) = last l.
 Proof. by rewrite <-last_reverse, reverse_involutive. Qed.
 Lemma head_Some_elem_of l x :