diff --git a/theories/list.v b/theories/list.v
index 5c66a5bfa14e949e9b8c89ddd435d655ff70b7ad..e0f6ede20c2d20929d1425310d940ad8d848204e 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -983,6 +983,11 @@ Proof.
   - intros [-> Hi]. revert i Hi.
     induction n; intros [|?]; naive_solver auto with lia.
 Qed.
+Lemma elem_of_replicate n x y : y ∈ replicate n x ↔ y = x ∧ n ≠ 0.
+Proof.
+  rewrite elem_of_list_lookup, Nat.neq_0_lt_0.
+  setoid_rewrite lookup_replicate; naive_solver eauto with lia.
+Qed.
 Lemma lookup_replicate_1 n x y i :
   replicate n x !! i = Some y → y = x ∧ i < n.
 Proof. by rewrite lookup_replicate. Qed.