diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5fab43e3153b408e8cb5a7d8719ac726129780b9..701574926066c5f0bf2dcd8e75516409a5cede6b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,6 +10,9 @@ lemma.
 * Add lemmas `big_opS_gset_to_gmap` and `big_opS_gset_to_gmap_L`, which rewrite
   between `gset_to_gmap` and big set ops of singleton maps.  (by Isaac van
   Bakel)
+* Add lemmas `discrete_fun_update` and `discrete_fun_updateP`, which updates an
+  abitrary `discrete_fun` to another. For `discrete_fun_updateP`, this requires
+  the domain to be finite, similar to `discrete_fun_included_spec`. (by Janggun Lee)
 
 **Changes in `proofmode`:**
 
diff --git a/iris/algebra/functions.v b/iris/algebra/functions.v
index 6aa92d2f9482dd47069a99158b0c9f5cce948a7a..210c1bffe24c9e27e0b54a92c2a498acdad7fca0 100644
--- a/iris/algebra/functions.v
+++ b/iris/algebra/functions.v
@@ -161,4 +161,23 @@ Section cmra.
     rewrite !cmra_update_updateP;
       eauto using discrete_fun_singleton_updateP_empty with subst.
   Qed.
+
+  Lemma discrete_fun_updateP `{!Finite A} f P Q :
+    (∀ a, f a ~~>: P a) → (∀ f', (∀ a, P a (f' a)) → Q f') → f ~~>: Q.
+  Proof.
+    repeat setoid_rewrite cmra_total_updateP. intros Hf HP n h Hh.
+    destruct (finite_choice
+      (λ a y, P a y ∧ ✓{n} (y ⋅ (h a)))) as [f' Hf']; first naive_solver.
+    naive_solver.
+  Qed.
+  Lemma discrete_fun_updateP' `{!Finite A} f P :
+    (∀ a, f a ~~>: P a) → f ~~>: λ f', ∀ a, P a (f' a).
+  Proof. eauto using discrete_fun_updateP. Qed.
+
+  Lemma discrete_fun_update f g :
+    (∀ a, f a ~~> g a) → f ~~> g.
+  Proof.
+    repeat setoid_rewrite cmra_total_update.
+    intros Hfg n h Hh a. apply (Hfg a), Hh.
+  Qed.
 End cmra.