diff --git a/iris/algebra/local_updates.v b/iris/algebra/local_updates.v
index dd679d26ff1cade494e850a338e354a670b714e5..3bd542e8cc2dae3cf5644891ef7e1c2f4ef7c9a4 100644
--- a/iris/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -137,6 +137,19 @@ Section updates_unital.
   Proof. rewrite -{2}(right_id ε op x). by apply cancel_local_update. Qed.
 End updates_unital.
 
+(** * Unit *)
+Lemma unit_local_update (x y x' y' : unit) : (x, y) ~l~> (x', y').
+Proof. destruct x,y,x',y'; reflexivity. Qed.
+
+(** * Dependently-typed functions over a discrete domain *)
+Lemma discrete_fun_local_update {A} {B : A → ucmra} (f g f' g' : discrete_fun B) :
+  (∀ x : A, (f x, g x) ~l~> (f' x, g' x)) →
+  (f, g) ~l~> (f', g').
+Proof.
+  setoid_rewrite local_update_unital. intros Hupd n h Hf Hg.
+  split=> x; eapply Hupd, Hg; eauto.
+Qed.
+
 (** * Product *)
 Lemma prod_local_update {A B : cmra} (x y x' y' : A * B) :
   (x.1,y.1) ~l~> (x'.1,y'.1) → (x.2,y.2) ~l~> (x'.2,y'.2) →