diff --git a/theories/list.v b/theories/list.v
index 0eeb08aa4d5f9fdaa537cb31e9a96677dab76636..04c85ce6a45fa2cc362d0c6775f40425a5e3463a 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3935,6 +3935,9 @@ Section fmap.
   Proof. intros; induction l; f_equal/=; auto. Qed.
   Lemma list_lookup_fmap l i : (f <$> l) !! i = f <$> (l !! i).
   Proof. revert i. induction l; intros [|n]; by try revert n. Qed.
+  Lemma list_lookup_fmap_Some l i x :
+    (f <$> l) !! i =  Some x ↔ ∃ y, l !! i = Some y ∧ x = f y.
+  Proof. by rewrite list_lookup_fmap, fmap_Some. Qed.
   Lemma list_lookup_total_fmap `{!Inhabited A, !Inhabited B} l i :
     i < length l → (f <$> l) !!! i = f (l !!! i).
   Proof.
@@ -4305,6 +4308,9 @@ Section imap.
     revert f i. induction l as [|x l IH]; intros f [|i]; f_equal/=; auto.
     by rewrite IH.
   Qed.
+  Lemma list_lookup_imap_Some l i x :
+    imap f l !! i = Some x ↔ ∃ y, l !! i = Some y ∧ x = f i y.
+  Proof. by rewrite list_lookup_imap, fmap_Some. Qed.
   Lemma list_lookup_total_imap `{!Inhabited A, !Inhabited B} l i :
     i < length l → imap f l !!! i = f i (l !!! i).
   Proof.