From cb3996f80e10798925e6841209bdbb0a040cbabf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Oct 2023 10:22:07 +0200
Subject: [PATCH] Add lemma `later_map_Next`.

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

diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index d64a63f82..53b19a8f7 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1413,6 +1413,10 @@ Global Instance later_map_proper {A B : ofe} (f : A → B) :
   Proper ((≡) ==> (≡)) f →
   Proper ((≡) ==> (≡)) (later_map f).
 Proof. solve_proper. Qed.
+
+Lemma later_map_Next {A B : ofe} (f : A → B) x :
+  later_map f (Next x) = Next (f x).
+Proof. done. Qed.
 Lemma later_map_id {A} (x : later A) : later_map id x = x.
 Proof. by destruct x. Qed.
 Lemma later_map_compose {A B C} (f : A → B) (g : B → C) (x : later A) :
-- 
GitLab