diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index d23895b01c036567f78593dd12263d362b2813a4..96298f84aea4c76df7b681c521ac8b24e8ca4917 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -724,6 +724,20 @@ Proof.
   by destruct (m !! i) eqn:?; simpl; erewrite ?Hi by eauto.
 Qed.
 
+Lemma map_fmap_omap {A B C} (f : A → option B) (g : B → C) (m : M A) :
+  g <$> omap f m = omap (λ x, g <$> f x) m.
+Proof.
+  apply map_eq. intros i.
+  rewrite !lookup_fmap, !lookup_omap. destruct (m !! i); done.
+Qed.
+
+Lemma map_fmap_alt {A B} (f : A → B) (m : M A) :
+  f <$> m = omap (λ x, Some (f x)) m.
+Proof.
+  apply map_eq. intros i.
+  rewrite lookup_fmap, lookup_omap. destruct (m !! i); done.
+Qed.
+
 Lemma map_fmap_mono {A B} (f : A → B) (m1 m2 : M A) :
   m1 ⊆ m2 → f <$> m1 ⊆ f <$> m2.
 Proof.
@@ -1487,7 +1501,15 @@ Section more_merge.
   Proof. by intros; apply partial_alter_merge_r. Qed.
 End more_merge.
 
-(** Properties of the zip_with function *)
+Lemma merge_diag {A C} (f : option A → option A → option C) `{!DiagNone f} (m : M A) :
+  merge f m m = omap (λ x, f (Some x) (Some x)) m.
+Proof.
+  apply map_eq. intros i.
+  rewrite lookup_merge by done.
+  rewrite lookup_omap. destruct (m !! i); done.
+Qed.
+
+(** Properties of the [zip_with] and [zip] functions *)
 Lemma map_lookup_zip_with {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i :
   map_zip_with f m1 m2 !! i = (x ← m1 !! i; y ← m2 !! i; Some (f x y)).
 Proof.
@@ -1585,6 +1607,17 @@ Proof.
   destruct (Hm k) as [y ->]; [by eauto|]. by f_equal/=.
 Qed.
 
+Lemma map_zip_with_diag {A C} (f : A → A → C) m :
+  map_zip_with f m m = (λ x, f x x) <$> m.
+Proof.
+  unfold map_zip_with. rewrite merge_diag by naive_solver.
+  rewrite map_fmap_alt. done.
+Qed.
+
+Lemma map_zip_diag {A} (m : M A) :
+  map_zip m m = (λ x, (x, x)) <$> m.
+Proof. apply map_zip_with_diag. Qed.
+
 (** ** Properties on the [map_relation] relation *)
 Section Forall2.
   Context {A B} (R : A → B → Prop) (P : A → Prop) (Q : B → Prop).
diff --git a/theories/list.v b/theories/list.v
index 1ce468019ca5eb5ebeaafdef822ab3272495d48d..8977f94c3c37815d021b6c983d757161dee5d72d 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3461,6 +3461,10 @@ Section fmap.
     destruct (IH l) as (l1&l2&->&->&->); [done|]. by exists (x :: l1), l2.
   Qed.
 
+  Lemma list_fmap_alt l :
+    f <$> l = omap (λ x, Some (f x)) l.
+  Proof. induction l; simplify_eq/=; done. Qed.
+
   Lemma fmap_length l : length (f <$> l) = length l.
   Proof. by induction l; f_equal/=. Qed.
   Lemma fmap_reverse l : f <$> reverse l = reverse (f <$> l).