diff --git a/CHANGELOG.md b/CHANGELOG.md
index 32d2f14cd8c367fb5987ebe5a0e5d3f0993e2dcf..cde49afa00027021953040452d0bea0752809627 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -13,6 +13,7 @@ API-breaking change is listed.
   `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
 - Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
   `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
+- Add `app_nil_r_inv` and `app_nil_l_inv` lemmas. (by Kimaya Bedarkar)
 
 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/stdpp/list.v b/stdpp/list.v
index 4a96bd886bcf83bd1377c6f4ce4ced2b13e2387b..9f9d0dad0ea22865166522415ccf925334d39c67 100644
--- a/stdpp/list.v
+++ b/stdpp/list.v
@@ -501,6 +501,10 @@ Proof. intro. apply app_nil_r. Qed.
 
 Lemma app_nil l1 l2 : l1 ++ l2 = [] ↔ l1 = [] ∧ l2 = [].
 Proof. split; [apply app_eq_nil|]. by intros [-> ->]. Qed.
+Lemma app_nil_l_inv l1 l2 : l1 ++ l2 = [] → l1 = [].
+Proof. by rewrite app_nil; intros [-> _]. Qed.
+Lemma app_nil_r_inv l1 l2 : l1 ++ l2 = [] → l2 = [].
+Proof. by rewrite app_nil; intros [_ ->]. Qed.
 Lemma app_singleton l1 l2 x :
   l1 ++ l2 = [x] ↔ l1 = [] ∧ l2 = [x] ∨ l1 = [x] ∧ l2 = [].
 Proof. split; [apply app_eq_unit|]. by intros [[-> ->]|[-> ->]]. Qed.