diff --git a/algebra/list.v b/algebra/list.v
index 269c6537610d834d3914347604b8cf293b5b70cc..44f4c440608ffbea6a1515910785ea0b2a29a562 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -360,6 +360,10 @@ Section properties.
       + rewrite !(cons_middle _ l1 l2) !assoc.
         rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
   Qed.
+
+  Lemma list_singleton_local_update i x y ml :
+    x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
+  Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
 End properties.
 
 (** Functor *)