diff --git a/stdpp/fin_maps.v b/stdpp/fin_maps.v
index 8056df977aa20f33a6c0601b9f1722587b5f2bc0..5adad1a9d45e968ac8e36b1277a8e630c80892d6 100644
--- a/stdpp/fin_maps.v
+++ b/stdpp/fin_maps.v
@@ -2301,7 +2301,7 @@ Qed.
 Global Instance map_union_idemp {A} : IdemP (=@{M A}) (∪).
 Proof. intros ?. by apply union_with_idemp. Qed.
 Lemma lookup_union {A} (m1 m2 : M A) i :
-  (m1 ∪ m2) !! i = union_with (λ x _, Some x) (m1 !! i) (m2 !! i).
+  (m1 ∪ m2) !! i = (m1 !! i) ∪ (m2 !! i).
 Proof. apply lookup_union_with. Qed.
 Lemma lookup_union_r {A} (m1 m2 : M A) i :
   m1 !! i = None → (m1 ∪ m2) !! i = m2 !! i.
diff --git a/stdpp/option.v b/stdpp/option.v
index 0189d77e2c2e70245f553cfab4525db1d7c4f537..4e4662d0601b6e519e38b32a323a0af2340308b0 100644
--- a/stdpp/option.v
+++ b/stdpp/option.v
@@ -299,6 +299,17 @@ Global Instance option_union {A} : Union (option A) := union_with (λ x _, Some
 Lemma option_union_Some {A} (mx my : option A) z :
   mx ∪ my = Some z → mx = Some z ∨ my = Some z.
 Proof. destruct mx, my; naive_solver. Qed.
+Lemma option_union_Some_l {A} x (my : option A) :
+  (Some x) ∪ my = Some x.
+Proof. destruct my; done. Qed.
+Lemma option_union_Some_r {A} (mx : option A) y :
+  mx ∪ (Some y) = Some (default y mx).
+Proof. destruct mx; done. Qed.
+
+Global Instance option_union_left_id {A} : LeftId (=@{option A}) None union.
+Proof. by intros [?|]. Qed.
+Global Instance option_union_right_id {A} : RightId (=@{option A}) None union.
+Proof. by intros [?|]. Qed.
 
 Section union_intersection_difference.
   Context {A} (f : A → A → option A).
@@ -310,10 +321,18 @@ Section union_intersection_difference.
   Global Instance union_with_comm :
     Comm (=) f → Comm (=@{option A}) (union_with f).
   Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
+  (* These are duplicates of the above LeftId/RightId instances, but easier to
+  find with SearchAbout. *)
+  Lemma union_with_None_l my : union_with f None my = my.
+  Proof. destruct my; done. Qed.
+  Lemma union_with_None_r mx : union_with f mx None = mx.
+  Proof. destruct mx; done. Qed.
+
   Global Instance intersection_with_left_ab : LeftAbsorb (=) None (intersection_with f).
   Proof. by intros [?|]. Qed.
   Global Instance intersection_with_right_ab : RightAbsorb (=) None (intersection_with f).
   Proof. by intros [?|]. Qed.
+
   Global Instance difference_with_comm :
     Comm (=) f → Comm (=@{option A}) (intersection_with f).
   Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.