diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index d64a63f82088238c31f643490f2d8e272dcac6c0..53b19a8f73665b4b3dc65d1be536ffff5f41c43d 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) :