diff --git a/CHANGELOG.md b/CHANGELOG.md
index 701574926066c5f0bf2dcd8e75516409a5cede6b..286da8513db2856d9c4a911d13fa3867e7049cf2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -13,6 +13,8 @@ lemma.
 * 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)
+* Add lemmas `discrete_fun_singleton_valid` and `discrete_fun_singleton_unit`, which simplify 
+  cmra validity and unit used with `discrete_fun_singleton`. (by Janggun Lee)
 
 **Changes in `proofmode`:**
 
diff --git a/iris/algebra/functions.v b/iris/algebra/functions.v
index 210c1bffe24c9e27e0b54a92c2a498acdad7fca0..4b0c2dc031ae5b554b493b6af9bbc40e45e82ba4 100644
--- a/iris/algebra/functions.v
+++ b/iris/algebra/functions.v
@@ -86,6 +86,16 @@ Section cmra.
       rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne //.
     by apply ucmra_unit_validN.
   Qed.
+  Lemma discrete_fun_singleton_valid x (y : B x) : ✓ discrete_fun_singleton x y ↔ ✓ y.
+  Proof.
+    by rewrite !cmra_valid_validN; setoid_rewrite discrete_fun_singleton_validN.
+  Qed.
+
+  Lemma discrete_fun_singleton_unit x : discrete_fun_singleton x (ε : B x) ≡ ε.
+  Proof.
+    move=>x'; destruct (decide (x = x')) as [->|];
+      by rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne.
+  Qed.
 
   Lemma discrete_fun_singleton_core x (y : B x) :
     core (discrete_fun_singleton x y) ≡ discrete_fun_singleton x (core y).