From 5cd932353cad5ca0eaf9c5f2879dc8796ce131dc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 17 Jun 2016 01:40:53 +0200
Subject: [PATCH] Prove list_singleton_local_update.

---
 algebra/list.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/algebra/list.v b/algebra/list.v
index 269c65376..44f4c4406 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 *)
-- 
GitLab