diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8629231f67718e42fdc87bbc1745f50dbbbe841b..80799303dfbe12b3049ec2248f2e482babcd9091 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -61,6 +61,13 @@ API-breaking change is listed.
 - Rename instances `option_mbind_proper` → `option_bind_proper` and
   `option_mjoin_proper` → `option_join_proper` to be consistent with similar
   instances for sets and lists.
+- Drop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface.
+  + Drop `DiagNone` class.
+  + Add `merge_proper` instance.
+  + Simplify lemmas about `merge` by dropping the `DiagNone` precondition.
+  + Generalize lemmas `partial_alter_merge`, `partial_alter_merge_l`, and
+    `partial_alter_merge_r`.
+  + Drop unused `merge_assoc'` instance.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 9a96e8abf8fab4448409c2befa4f56d8b6ef1e29..ea77ec1a62149cac76d80850201dcde08dbb5786 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -30,6 +30,15 @@ Class FinMapToList K A M := map_to_list: M → list (K * A).
 Global Hint Mode FinMapToList ! - - : typeclass_instances.
 Global Hint Mode FinMapToList - - ! : typeclass_instances.
 
+(** The function [diag_None f] is used in the specification and lemmas of
+[merge f]. It lifts a function [f : option A → option B → option C] by returning
+[None] if both arguments are [None], to make sure that in [merge f m1 m2], the
+function [f] can only operate on elements that are in the domain of either [m1]
+or [m2]. *)
+Definition diag_None {A B C} (f : option A → option B → option C)
+    (mx : option A) (my : option B) : option C :=
+  match mx, my with None, None => None | _, _ => f mx my end.
+
 Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
     PartialAlter K A (M A), OMap M, Merge M, ∀ A, FinMapToList K A (M A),
     EqDecision K} := {
@@ -45,9 +54,8 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
     (i,x) ∈ map_to_list m ↔ m !! i = Some x;
   lookup_omap {A B} (f : A → option B) (m : M A) i :
     omap f m !! i = m !! i ≫= f;
-  lookup_merge {A B C} (f : option A → option B → option C)
-      `{!DiagNone f} (m1 : M A) (m2 : M B) i :
-    merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
+  lookup_merge {A B C} (f : option A → option B → option C) (m1 : M A) (m2 : M B) i :
+    merge f m1 m2 !! i = diag_None f (m1 !! i) (m2 !! i)
 }.
 
 (** * Derived operations *)
@@ -225,30 +233,28 @@ Section setoid.
     intros ?? Hf; apply partial_alter_proper.
     by destruct 1; constructor; apply Hf.
   Qed.
-
-  Lemma merge_ext `{Equiv B, Equiv C} (f g : option A → option B → option C)
-      `{!DiagNone f, !DiagNone g} :
-    ((≡) ==> (≡) ==> (≡))%signature f g →
-    ((≡) ==> (≡) ==> (≡@{M _}))%signature (merge f) (merge g).
+  Global Instance merge_proper `{Equiv B, Equiv C} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B}) ==> (≡@{M C})) merge.
   Proof.
-    by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf.
+    intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
+    destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
   Qed.
   Global Instance union_with_proper :
     Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) union_with.
   Proof.
-    intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
+    intros ?? Hf. apply merge_proper.
     by do 2 destruct 1; first [apply Hf | constructor].
   Qed.
   Global Instance intersection_with_proper :
     Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) intersection_with.
   Proof.
-    intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
+    intros ?? Hf. apply merge_proper.
     by do 2 destruct 1; first [apply Hf | constructor].
   Qed.
   Global Instance difference_with_proper :
     Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡@{M A})) difference_with.
   Proof.
-    intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
+    intros ?? Hf. apply merge_proper.
     by do 2 destruct 1; first [apply Hf | constructor].
   Qed.
   Global Instance union_proper : Proper ((≡) ==> (≡) ==>(≡@{M A})) union.
@@ -262,7 +268,7 @@ Section setoid.
     Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{M A}) ==> (≡@{M B}) ==> (≡@{M C}))
       map_zip_with.
   Proof.
-    intros f1 f2 Hf m1 m1' Hm1 m2 m2' Hm2. apply merge_ext; try done.
+    intros f1 f2 Hf. apply merge_proper.
     destruct 1; destruct 1; repeat f_equiv; constructor || by apply Hf.
   Qed.
 
@@ -1569,7 +1575,7 @@ End map_Forall.
 
 (** ** Properties of the [merge] operation *)
 Section merge.
-  Context {A} (f : option A → option A → option A) `{!DiagNone f}.
+  Context {A} (f : option A → option A → option A).
   Implicit Types m : M A.
 
   (** These instances can in many cases not be applied automatically due to Coq
@@ -1577,87 +1583,95 @@ Section merge.
   specific operations such as union or difference in the rest of this file. *)
   Global Instance: LeftId (=) None f → LeftId (=) (∅ : M A) (merge f).
   Proof.
-    intros ??. apply map_eq. intros.
-    by rewrite !(lookup_merge f), lookup_empty, (left_id_L None f).
+    intros ? m. apply map_eq; intros i.
+    rewrite !lookup_merge, lookup_empty. destruct (m !! i); by simpl.
   Qed.
   Global Instance: RightId (=) None f → RightId (=) (∅ : M A) (merge f).
   Proof.
-    intros ??. apply map_eq. intros.
-    by rewrite !(lookup_merge f), lookup_empty, (right_id_L None f).
+    intros ? m. apply map_eq; intros i.
+    rewrite !lookup_merge, lookup_empty. destruct (m !! i); by simpl.
   Qed.
   Global Instance: LeftAbsorb (=) None f → LeftAbsorb (=) (∅ : M A) (merge f).
   Proof.
-    intros ??. apply map_eq. intros.
-    by rewrite !(lookup_merge f), lookup_empty, (left_absorb_L None f).
+    intros ? m. apply map_eq; intros i.
+    rewrite !lookup_merge, lookup_empty. destruct (m !! i); by simpl.
   Qed.
   Global Instance: RightAbsorb (=) None f → RightAbsorb (=) (∅ : M A) (merge f).
   Proof.
-    intros ??. apply map_eq. intros.
-    by rewrite !(lookup_merge f), lookup_empty, (right_absorb_L None f).
+    intros ? m. apply map_eq; intros i.
+    rewrite !lookup_merge, lookup_empty. destruct (m !! i); by simpl.
   Qed.
   Lemma merge_comm m1 m2 :
     (∀ i, f (m1 !! i) (m2 !! i) = f (m2 !! i) (m1 !! i)) →
     merge f m1 m2 = merge f m2 m1.
-  Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
+  Proof.
+    intros Hm. apply map_eq; intros i. specialize (Hm i).
+    rewrite !lookup_merge. by destruct (m1 !! i), (m2 !! i).
+  Qed.
   Global Instance merge_comm' : Comm (=) f → Comm (=@{M _}) (merge f).
   Proof. intros ???. apply merge_comm. intros. by apply (comm f). Qed.
   Lemma merge_assoc m1 m2 m3 :
-    (∀ i, f (m1 !! i) (f (m2 !! i) (m3 !! i)) =
-          f (f (m1 !! i) (m2 !! i)) (m3 !! i)) →
+    (∀ i, diag_None f (m1 !! i) (diag_None f (m2 !! i) (m3 !! i)) =
+          diag_None f (diag_None f (m1 !! i) (m2 !! i)) (m3 !! i)) →
     merge f m1 (merge f m2 m3) = merge f (merge f m1 m2) m3.
-  Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
-  Global Instance merge_assoc' : Assoc (=) f → Assoc (=@{M _}) (merge f).
-  Proof. intros ????. apply merge_assoc. intros. by apply (assoc_L f). Qed.
+  Proof.
+    intros Hm. apply map_eq; intros i. specialize (Hm i).
+    by rewrite !lookup_merge.
+  Qed.
   Lemma merge_idemp m1 :
     (∀ i, f (m1 !! i) (m1 !! i) = m1 !! i) → merge f m1 m1 = m1.
-  Proof. intros. apply map_eq. intros. by rewrite !(lookup_merge f). Qed.
+  Proof.
+    intros Hm. apply map_eq; intros i. specialize (Hm i).
+    rewrite !lookup_merge. by destruct (m1 !! i).
+  Qed.
   Global Instance merge_idemp' : IdemP (=) f → IdemP (=@{M _}) (merge f).
   Proof. intros ??. apply merge_idemp. intros. by apply (idemp f). Qed.
 End merge.
 
 Section more_merge.
-  Context {A B C} (f : option A → option B → option C) `{!DiagNone f}.
+  Context {A B C} (f : option A → option B → option C).
 
   Lemma merge_Some (m1 : M A) (m2 : M B) (m : M C) :
+    f None None = None →
     (∀ i, m !! i = f (m1 !! i) (m2 !! i)) ↔ merge f m1 m2 = m.
   Proof.
-    split; [|intros <-; apply (lookup_merge _) ].
-    intros Hlookup. apply map_eq; intros. rewrite Hlookup. apply (lookup_merge _).
+   intros. rewrite map_eq_iff. apply forall_proper; intros i.
+   rewrite lookup_merge. destruct (m1 !! i), (m2 !! i); naive_solver congruence.
   Qed.
   Lemma merge_empty : merge f (∅ : M A) (∅ : M B) = ∅.
-  Proof. apply map_eq. intros. by rewrite !(lookup_merge f), !lookup_empty. Qed.
+  Proof. apply map_eq. intros. by rewrite !lookup_merge, !lookup_empty. Qed.
   Lemma partial_alter_merge g g1 g2 (m1 : M A) (m2 : M B) i :
-    g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (g2 (m2 !! i)) →
+    g (diag_None f (m1 !! i) (m2 !! i)) = diag_None f (g1 (m1 !! i)) (g2 (m2 !! i)) →
     partial_alter g i (merge f m1 m2) =
       merge f (partial_alter g1 i m1) (partial_alter g2 i m2).
   Proof.
     intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
-    - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
-    - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+    - by rewrite lookup_merge, !lookup_partial_alter, !lookup_merge.
+    - by rewrite lookup_merge, !lookup_partial_alter_ne, lookup_merge.
   Qed.
   Lemma partial_alter_merge_l g g1 (m1 : M A) (m2 : M B) i :
-    g (f (m1 !! i) (m2 !! i)) = f (g1 (m1 !! i)) (m2 !! i) →
+    g (diag_None f (m1 !! i) (m2 !! i)) = diag_None f (g1 (m1 !! i)) (m2 !! i) →
     partial_alter g i (merge f m1 m2) = merge f (partial_alter g1 i m1) m2.
   Proof.
     intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
-    - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
-    - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+    - by rewrite lookup_merge, !lookup_partial_alter, !lookup_merge.
+    - by rewrite lookup_merge, !lookup_partial_alter_ne, lookup_merge.
   Qed.
   Lemma partial_alter_merge_r g g2 (m1 : M A) (m2 : M B) i :
-    g (f (m1 !! i) (m2 !! i)) = f (m1 !! i) (g2 (m2 !! i)) →
+    g (diag_None f (m1 !! i) (m2 !! i)) = diag_None f (m1 !! i) (g2 (m2 !! i)) →
     partial_alter g i (merge f m1 m2) = merge f m1 (partial_alter g2 i m2).
   Proof.
     intro. apply map_eq. intros j. destruct (decide (i = j)); subst.
-    - by rewrite (lookup_merge _), !lookup_partial_alter, !(lookup_merge _).
-    - by rewrite (lookup_merge _), !lookup_partial_alter_ne, (lookup_merge _).
+    - by rewrite lookup_merge, !lookup_partial_alter, !lookup_merge.
+    - by rewrite lookup_merge, !lookup_partial_alter_ne, lookup_merge.
   Qed.
   Lemma insert_merge (m1 : M A) (m2 : M B) i x y z :
     f (Some y) (Some z) = Some x →
     <[i:=x]>(merge f m1 m2) = merge f (<[i:=y]>m1) (<[i:=z]>m2).
-  Proof. by intros; apply partial_alter_merge. Qed.
+  Proof. intros; by apply partial_alter_merge. Qed.
   Lemma delete_merge (m1 : M A) (m2 : M B) i :
     delete i (merge f m1 m2) = merge f (delete i m1) (delete i m2).
-  Proof. by intros; apply partial_alter_merge. Qed.
+  Proof. intros; by apply partial_alter_merge. Qed.
   Lemma merge_singleton i x y z :
     f (Some y) (Some z) = Some x →
     merge f ({[i := y]} : M A) ({[i := z]} : M B) = {[i := x]}.
@@ -1671,37 +1685,34 @@ Section more_merge.
   Lemma insert_merge_r (m1 : M A) (m2 : M B) i x z :
     f (m1 !! i) (Some z) = Some x →
     <[i:=x]>(merge f m1 m2) = merge f m1 (<[i:=z]>m2).
-  Proof. by intros; apply partial_alter_merge_r. Qed.
+  Proof. intros; apply partial_alter_merge_r. by destruct (m1 !! i). Qed.
 
   Lemma fmap_merge {D} (g : C → D) (m1 : M A) (m2 : M B) :
     g <$> merge f m1 m2 = merge (λ mx1 mx2, g <$> f mx1 mx2) m1 m2.
   Proof.
-    assert (DiagNone (λ mx1 mx2, g <$> f mx1 mx2)).
-    { unfold DiagNone. by rewrite diag_none. }
-    apply map_eq; intros i. by rewrite lookup_fmap, !lookup_merge by done.
+    apply map_eq; intros i. rewrite lookup_fmap, !lookup_merge.
+    by destruct (m1 !! i), (m2 !! i).
   Qed.
   Lemma omap_merge {D} (g : C → option D) (m1 : M A) (m2 : M B) :
     omap g (merge f m1 m2) = merge (λ mx1 mx2, f mx1 mx2 ≫= g) m1 m2.
   Proof.
-    assert (DiagNone (λ mx1 mx2, f mx1 mx2 ≫= g)).
-    { unfold DiagNone. by rewrite diag_none. }
-    apply map_eq; intros i. by rewrite lookup_omap, !lookup_merge by done.
+    apply map_eq; intros i. rewrite lookup_omap, !lookup_merge.
+    by destruct (m1 !! i), (m2 !! i).
   Qed.
 End more_merge.
 
-Lemma merge_diag {A C} (f : option A → option A → option C) `{!DiagNone f} (m : M A) :
+Lemma merge_diag {A C} (f : option A → option A → option C) (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.
+  rewrite lookup_merge, lookup_omap. by destruct (m !! i).
 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.
-  unfold map_zip_with. rewrite lookup_merge by done.
+  unfold map_zip_with. rewrite lookup_merge.
   by destruct (m1 !! i), (m2 !! i).
 Qed.
 Lemma map_lookup_zip_with_Some {A B C} (f : A → B → C) (m1 : M A) (m2 : M B) i z :
@@ -1744,7 +1755,7 @@ Lemma map_zip_with_fmap_2 {A B' B C} (f : A → B → C)
     (g : B' → B) (m1 : M A) (m2 : M B') :
   map_zip_with f m1 (g <$> m2) = map_zip_with (λ x y, f x (g y)) m1 m2.
 Proof.
-  rewrite <- (map_fmap_id m1) at 1. by rewrite map_zip_with_fmap.
+  rewrite <-(map_fmap_id m1) at 1. by rewrite map_zip_with_fmap.
 Qed.
 
 Lemma map_fmap_zip_with {A B C D} (f : A → B → C) (g : C → D)
@@ -1801,10 +1812,7 @@ Qed.
 
 Lemma map_zip_with_diag {A C} (f : A → A → C) (m : M A) :
   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.
+Proof. unfold map_zip_with. by rewrite merge_diag, map_fmap_alt. Qed.
 
 Lemma map_zip_diag {A} (m : M A) :
   map_zip m m = (λ x, (x, x)) <$> m.
@@ -1826,10 +1834,10 @@ Section Forall2.
     map_relation R P Q m1 m2 ↔ map_Forall (λ _, Is_true) (merge f m1 m2).
   Proof.
     split.
-    - intros Hm i P'; rewrite lookup_merge by done; intros.
+    - intros Hm i P'; rewrite lookup_merge; intros.
       specialize (Hm i). destruct (m1 !! i), (m2 !! i);
         simplify_eq/=; auto using bool_decide_pack.
-    - intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm by done.
+    - intros Hm i. specialize (Hm i). rewrite lookup_merge in Hm.
       destruct (m1 !! i), (m2 !! i); simplify_eq/=; auto;
         by eapply bool_decide_unpack, Hm.
   Qed.
@@ -1848,7 +1856,7 @@ Section Forall2.
   Proof.
     split.
     - rewrite map_relation_alt, (map_not_Forall _). intros (i&?&Hm&?); exists i.
-      rewrite lookup_merge in Hm by done.
+      rewrite lookup_merge in Hm.
       destruct (m1 !! i), (m2 !! i); naive_solver auto 2 using bool_decide_pack.
     - unfold map_relation, option_relation.
       by intros [i[(x&y&?&?&?)|[(x&?&?&?)|(y&?&?&?)]]] Hm;
@@ -1956,7 +1964,10 @@ Section union_with.
 
   Lemma lookup_union_with m1 m2 i :
     union_with f m1 m2 !! i = union_with f (m1 !! i) (m2 !! i).
-  Proof. by rewrite <-(lookup_merge _). Qed.
+  Proof.
+    unfold union_with, map_union_with. rewrite lookup_merge.
+    by destruct (m1 !! i), (m2 !! i).
+  Qed.
   Lemma lookup_union_with_Some m1 m2 i z :
     union_with f m1 m2 !! i = Some z ↔
       (m1 !! i = Some z ∧ m2 !! i = None) ∨
@@ -1974,7 +1985,7 @@ Section union_with.
     (∀ i x y, m1 !! i = Some x → m2 !! i = Some y → f x y = f y x) →
     union_with f m1 m2 = union_with f m2 m1.
   Proof.
-    intros. apply (merge_comm _). intros i.
+    intros. apply merge_comm. intros i.
     destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
   Qed.
   Global Instance: Comm (=) f → Comm (=@{M A}) (union_with f).
@@ -1982,7 +1993,7 @@ Section union_with.
   Lemma union_with_idemp m :
     (∀ i x, m !! i = Some x → f x x = Some x) → union_with f m m = m.
   Proof.
-    intros. apply (merge_idemp _). intros i.
+    intros. apply merge_idemp. intros i.
     destruct (m !! i) eqn:?; simpl; eauto.
   Qed.
   Lemma alter_union_with (g : A → A) m1 m2 i :
@@ -1990,7 +2001,7 @@ Section union_with.
     alter g i (union_with f m1 m2) =
       union_with f (alter g i m1) (alter g i m2).
   Proof.
-    intros. apply (partial_alter_merge _).
+    intros. apply partial_alter_merge.
     destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; simpl; eauto.
   Qed.
   Lemma alter_union_with_l (g : A → A) m1 m2 i :
@@ -1998,7 +2009,7 @@ Section union_with.
     (∀ y, m1 !! i = None → m2 !! i = Some y → g y = y) →
     alter g i (union_with f m1 m2) = union_with f (alter g i m1) m2.
   Proof.
-    intros. apply (partial_alter_merge_l _).
+    intros. apply partial_alter_merge_l.
     destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal/=; auto.
   Qed.
   Lemma alter_union_with_r (g : A → A) m1 m2 i :
@@ -2006,12 +2017,12 @@ Section union_with.
     (∀ x, m1 !! i = Some x → m2 !! i = None → g x = x) →
     alter g i (union_with f m1 m2) = union_with f m1 (alter g i m2).
   Proof.
-    intros. apply (partial_alter_merge_r _).
+    intros. apply partial_alter_merge_r.
     destruct (m1 !! i) eqn:?, (m2 !! i) eqn:?; f_equal/=; auto.
   Qed.
   Lemma delete_union_with m1 m2 i :
     delete i (union_with f m1 m2) = union_with f (delete i m1) (delete i m2).
-  Proof. by apply (partial_alter_merge _). Qed.
+  Proof. by apply partial_alter_merge. Qed.
   Lemma foldr_delete_union_with (m1 m2 : M A) is :
     foldr delete (union_with f m1 m2) is =
       union_with f (foldr delete m1 is) (foldr delete m2 is).
@@ -2027,13 +2038,13 @@ Section union_with.
     m2 !! i = None → <[i:=x]>(union_with f m1 m2) = union_with f (<[i:=x]>m1) m2.
   Proof.
     intros Hm2. unfold union_with, map_union_with.
-    by erewrite (insert_merge_l _) by (by rewrite Hm2).
+    by erewrite insert_merge_l by (by rewrite Hm2).
   Qed.
   Lemma insert_union_with_r m1 m2 i x :
     m1 !! i = None → <[i:=x]>(union_with f m1 m2) = union_with f m1 (<[i:=x]>m2).
   Proof.
     intros Hm1. unfold union_with, map_union_with.
-    by erewrite (insert_merge_r _) by (by rewrite Hm1).
+    by erewrite insert_merge_r by (by rewrite Hm1).
   Qed.
 End union_with.
 
@@ -2043,7 +2054,7 @@ Global Instance map_union_empty {A} : RightId (=@{M A}) ∅ (∪) := _.
 Global Instance map_union_assoc {A} : Assoc (=@{M A}) (∪).
 Proof.
   intros m1 m2 m3. unfold union, map_union, union_with, map_union_with.
-  apply (merge_assoc _). intros i.
+  apply merge_assoc. intros i.
   by destruct (m1 !! i), (m2 !! i), (m3 !! i).
 Qed.
 Global Instance map_union_idemp {A} : IdemP (=@{M A}) (∪).
@@ -2425,7 +2436,10 @@ Section intersection_with.
   Proof. unfold intersection_with, map_intersection_with. apply _. Qed.
   Lemma lookup_intersection_with m1 m2 i :
     intersection_with f m1 m2 !! i = intersection_with f (m1 !! i) (m2 !! i).
-  Proof. by rewrite <-(lookup_merge _). Qed.
+  Proof.
+    unfold intersection_with, map_intersection_with. rewrite lookup_merge.
+    by destruct (m1 !! i), (m2 !! i).
+  Qed.
   Lemma lookup_intersection_with_Some m1 m2 i z :
     intersection_with f m1 m2 !! i = Some z ↔
       (∃ x y, m1 !! i = Some x ∧ m2 !! i = Some y ∧ f x y = Some z).
@@ -2503,7 +2517,11 @@ Qed.
 (** ** Properties of the [difference_with] operation *)
 Lemma lookup_difference_with {A} (f : A → A → option A) (m1 m2 : M A) i :
   difference_with f m1 m2 !! i = difference_with f (m1 !! i) (m2 !! i).
-Proof. by rewrite <-lookup_merge by done. Qed.
+Proof.
+  unfold difference_with, map_difference_with. rewrite lookup_merge.
+  by destruct (m1 !! i), (m2 !! i).
+Qed.
+
 Lemma lookup_difference_with_Some {A} (f : A → A → option A) (m1 m2 : M A) i z :
   difference_with f m1 m2 !! i = Some z ↔
     (m1 !! i = Some z ∧ m2 !! i = None) ∨
@@ -2540,7 +2558,7 @@ Proof.
   rewrite map_subseteq_spec. intro Hm1m2. apply map_eq. intros i.
   apply option_eq. intros v. specialize (Hm1m2 i).
   unfold difference, map_difference, difference_with, map_difference_with.
-  rewrite lookup_union_Some_raw, (lookup_merge _).
+  rewrite lookup_union_Some_raw, lookup_merge.
   destruct (m1 !! i) as [x'|], (m2 !! i);
     try specialize (Hm1m2 x'); compute; intuition congruence.
 Qed.
@@ -2737,33 +2755,32 @@ Section kmap.
   Proof. apply kmap_partial_alter. Qed.
 
   Lemma kmap_merge {A B C} (g : option A → option B → option C)
-      `{!DiagNone g} (m1 : M1 A) (m2 : M1 B) :
+      (m1 : M1 A) (m2 : M1 B) :
     kmap f (merge g m1 m2) = merge g (kmap f m1) (kmap f m2).
   Proof.
     apply map_eq; intros j. apply option_eq; intros y.
-    rewrite (lookup_merge g), lookup_kmap_Some.
-    setoid_rewrite (lookup_merge g). split.
+    rewrite lookup_merge, lookup_kmap_Some.
+    setoid_rewrite lookup_merge. split.
     { intros [i [-> ?]]. by rewrite !lookup_kmap. }
     intros Hg. destruct (kmap f m1 !! j) as [x1|] eqn:Hm1.
     { apply lookup_kmap_Some in Hm1 as (i&->&Hm1i).
       exists i. split; [done|]. by rewrite Hm1i, <-lookup_kmap. }
-    destruct (kmap f m2 !! j) as [x2|] eqn:Hm2.
-    { apply lookup_kmap_Some in Hm2 as (i&->&Hm2i).
-      exists i. split; [done|]. by rewrite Hm2i, <-lookup_kmap, Hm1. }
-    unfold DiagNone in *. naive_solver.
+    destruct (kmap f m2 !! j) as [x2|] eqn:Hm2; [|naive_solver].
+    apply lookup_kmap_Some in Hm2 as (i&->&Hm2i).
+    exists i. split; [done|]. by rewrite Hm2i, <-lookup_kmap, Hm1.
   Qed.
   Lemma kmap_union_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
     kmap f (union_with g m1 m2)
     = union_with g (kmap f m1) (kmap f m2).
-  Proof. apply (kmap_merge _). Qed.
+  Proof. apply kmap_merge. Qed.
   Lemma kmap_intersection_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
     kmap f (intersection_with g m1 m2)
     = intersection_with g (kmap f m1) (kmap f m2).
-  Proof. apply (kmap_merge _). Qed.
+  Proof. apply kmap_merge. Qed.
   Lemma kmap_difference_with {A} (g : A → A → option A) (m1 m2 : M1 A) :
     kmap f (difference_with g m1 m2)
     = difference_with g (kmap f m1) (kmap f m2).
-  Proof. apply (kmap_merge _). Qed.
+  Proof. apply kmap_merge. Qed.
 
   Lemma kmap_union {A} (m1 m2 : M1 A) :
     kmap f (m1 ∪ m2) = kmap f m1 ∪ kmap f m2.
@@ -2773,7 +2790,7 @@ Section kmap.
   Proof. apply kmap_intersection_with. Qed.
   Lemma kmap_difference {A} (m1 m2 : M1 A) :
     kmap f (m1 ∖ m2) = kmap f m1 ∖ kmap f m2.
-  Proof. apply (kmap_merge _). Qed.
+  Proof. apply kmap_difference_with. Qed.
 
   Lemma kmap_zip_with {A B C} (g : A → B → C) (m1 : M1 A) (m2 : M1 B) :
     kmap f (map_zip_with g m1 m2) = map_zip_with g (kmap f m1) (kmap f m2).
diff --git a/theories/gmap.v b/theories/gmap.v
index 944fd3f622a635e4d24c579b8a4688d25402e8a9..f0f72d2af302a6b7d487997ef307d69dbe95f57b 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -83,18 +83,18 @@ Global Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f '(GMap m Hm
   GMap (omap f m) (gmap_omap_wf f m Hm).
 Lemma gmap_merge_wf `{Countable K} {A B C}
     (f : option A → option B → option C) m1 m2 :
-  let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
-  gmap_wf K m1 → gmap_wf K m2 → gmap_wf K (merge f' m1 m2).
+  gmap_wf K m1 → gmap_wf K m2 → gmap_wf K (merge f m1 m2).
 Proof.
-  intros f'; unfold gmap_wf; rewrite !bool_decide_spec.
-  intros Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
+  unfold gmap_wf; rewrite !bool_decide_spec.
+  intros Hm1 Hm2 p z. rewrite lookup_merge; intros.
   destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
 Qed.
-Global Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f '(GMap m1 Hm1) '(GMap m2 Hm2),
-  let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
-  GMap (merge f' m1 m2) (gmap_merge_wf f m1 m2 Hm1 Hm2).
-Global Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ '(GMap m _),
-  omap (λ '(i, x), (., x) <$> decode i) (map_to_list m).
+Global Instance gmap_merge `{Countable K} : Merge (gmap K) :=
+  λ A B C f '(GMap m1 Hm1) '(GMap m2 Hm2),
+    GMap (merge f m1 m2) (gmap_merge_wf f m1 m2 Hm1 Hm2).
+Global Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) :=
+  λ '(GMap m _),
+    omap (λ '(i, x), (., x) <$> decode i) (map_to_list m).
 
 (** * Instantiation of the finite map interface *)
 Global Instance gmap_finmap `{Countable K} : FinMap K (gmap K).
@@ -129,8 +129,7 @@ Proof.
     + intros; exists (encode i,x); simpl.
       by rewrite elem_of_map_to_list, decode_encode.
   - intros A B f [m Hm] i; apply (lookup_omap f m).
-  - intros A B C f ? [m1 Hm1] [m2 Hm2] i; unfold merge, lookup; simpl.
-    set (f' o1 o2 := match o1, o2 with None,None => None | _, _ => f o1 o2 end).
+  - intros A B C f [m1 Hm1] [m2 Hm2] i; unfold merge, lookup; simpl.
     by rewrite lookup_merge by done; destruct (m1 !! _), (m2 !! _).
 Qed.
 
diff --git a/theories/mapset.v b/theories/mapset.v
index 184839d831ca695ff844613edb2b0f8d8d0ce762..798f9761aa022431421a9e4bfa680ddb85dcbac2 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -120,7 +120,7 @@ Lemma elem_of_mapset_dom_with {A} (f : A → bool) m i :
   i ∈ mapset_dom_with f m ↔ ∃ x, m !! i = Some x ∧ f x.
 Proof.
   unfold mapset_dom_with, elem_of, mapset_elem_of.
-  simpl. rewrite lookup_merge by done. destruct (m !! i) as [a|].
+  simpl. rewrite lookup_merge, lookup_empty. destruct (m !! i) as [a|]; simpl.
   - destruct (Is_true_reflect (f a)); naive_solver.
   - naive_solver.
 Qed.
diff --git a/theories/natmap.v b/theories/natmap.v
index 404e52e0c6644b4524d597268327bac4c28cfaf5..9d56d247cdb4b0c932c567cb52e9ddc2d13da3ad 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -128,7 +128,7 @@ Definition natmap_merge_raw {A B C} (f : option A → option B → option C) :
   match l1, l2 with
   | [], l2 => natmap_omap_raw (f None ∘ Some) l2
   | l1, [] => natmap_omap_raw (flip f None ∘ Some) l1
-  | o1 :: l1, o2 :: l2 => natmap_cons_canon (f o1 o2) (go l1 l2)
+  | o1 :: l1, o2 :: l2 => natmap_cons_canon (diag_None f o1 o2) (go l1 l2)
   end.
 Lemma natmap_merge_wf {A B C} (f : option A → option B → option C) l1 l2 :
   natmap_wf l1 → natmap_wf l2 → natmap_wf (natmap_merge_raw f l1 l2).
@@ -136,9 +136,8 @@ Proof.
   revert l2. induction l1; intros [|??]; simpl;
     eauto using natmap_omap_raw_wf, natmap_cons_canon_wf, natmap_wf_inv.
 Qed.
-Lemma natmap_lookup_merge_raw {A B C} (f : option A → option B → option C)
-    l1 l2 i : f None None = None →
-  mjoin (natmap_merge_raw f l1 l2 !! i) = f (mjoin (l1 !! i)) (mjoin (l2 !! i)).
+Lemma natmap_lookup_merge_raw {A B C} (f : option A → option B → option C) l1 l2 i :
+  mjoin (natmap_merge_raw f l1 l2 !! i) = diag_None f (mjoin (l1 !! i)) (mjoin (l2 !! i)).
 Proof.
   intros. revert i l2. induction l1; intros [|?] [|??]; simpl;
     autorewrite with natmap; auto;
@@ -230,7 +229,7 @@ Proof.
   - intros ? [??]. by apply natmap_to_list_raw_nodup.
   - intros ? [??] ??. by apply natmap_elem_of_to_list_raw.
   - intros ??? [??] ?. by apply natmap_lookup_omap_raw.
-  - intros ????? [??] [??] ?. by apply natmap_lookup_merge_raw.
+  - intros ???? [??] [??] ?. apply natmap_lookup_merge_raw.
 Qed.
 
 Fixpoint strip_Nones {A} (l : list (option A)) : list (option A) :=
diff --git a/theories/nmap.v b/theories/nmap.v
index 2e1916d89780b8ffc47ec9be5d91313725517339..d68b188bd4e17010c77bcb8a9b15d7b3d66d2435 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -39,7 +39,7 @@ Global Instance Nomap: OMap Nmap := λ A B f t,
   match t with NMap o t => NMap (o ≫= f) (omap f t) end.
 Global Instance Nmerge: Merge Nmap := λ A B C f t1 t2,
   match t1, t2 with
-  | NMap o1 t1, NMap o2 t2 => NMap (f o1 o2) (merge f t1 t2)
+  | NMap o1 t1, NMap o2 t2 => NMap (diag_None f o1 o2) (merge f t1 t2)
   end.
 Global Instance Nfmap: FMap Nmap := λ A B f t,
   match t with NMap o t => NMap (f <$> o) (f <$> t) end.
@@ -74,7 +74,7 @@ Proof.
         destruct i as [|i]; simpl; [done |].
         intros. exists (i, x). by rewrite elem_of_map_to_list.
   - intros ?? f [??] [|?]; simpl; [done|]; apply (lookup_omap f).
-  - intros ??? f ? [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
+  - intros ??? f [??] [??] [|?]; simpl; [done|]; apply (lookup_merge f).
 Qed.
 
 (** * Finite sets *)
diff --git a/theories/option.v b/theories/option.v
index 179667b663daa6912372b80620143f29d8778ece..767426f172e95168de65cb553ffbad8b25858d22 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -302,18 +302,9 @@ 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.
 
-Class DiagNone {A B C} (f : option A → option B → option C) :=
-  diag_none : f None None = None.
-
 Section union_intersection_difference.
   Context {A} (f : A → A → option A).
 
-  Global Instance union_with_diag_none : DiagNone (union_with f).
-  Proof. reflexivity. Qed.
-  Global Instance intersection_with_diag_none : DiagNone (intersection_with f).
-  Proof. reflexivity. Qed.
-  Global Instance difference_with_diag_none : DiagNone (difference_with f).
-  Proof. reflexivity. Qed.
   Global Instance union_with_left_id : LeftId (=) None (union_with f).
   Proof. by intros [?|]. Qed.
   Global Instance union_with_right_id : RightId (=) None (union_with f).
diff --git a/theories/pmap.v b/theories/pmap.v
index f62d6c6c2f393df8d48f9296065436db54edf7a2..f269f482cec3454211aa5fec2ad30e7a9d51432a 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -99,7 +99,7 @@ Fixpoint Pmerge_raw {A B C} (f : option A → option B → option C)
   | PLeaf, t2 => Pomap_raw (f None ∘ Some) t2
   | t1, PLeaf => Pomap_raw (flip f None ∘ Some) t1
   | PNode o1 l1 r1, PNode o2 l2 r2 =>
-      PNode' (f o1 o2) (Pmerge_raw f l1 l2) (Pmerge_raw f r1 r2)
+      PNode' (diag_None f o1 o2) (Pmerge_raw f l1 l2) (Pmerge_raw f r1 r2)
   end.
 
 (** Proofs *)
@@ -241,14 +241,13 @@ Proof.
   revert i. induction t as [|o l IHl r IHr]; intros [i|i|]; simpl;
     rewrite ?PNode_lookup; simpl; auto.
 Qed.
-Lemma Pmerge_lookup {A B C} (f : option A → option B → option C)
-    (Hf : f None None = None) t1 t2 i :
-  Pmerge_raw f t1 t2 !! i = f (t1 !! i) (t2 !! i).
+Lemma Pmerge_lookup {A B C} (f : option A → option B → option C) t1 t2 i :
+  Pmerge_raw f t1 t2 !! i = diag_None f (t1 !! i) (t2 !! i).
 Proof.
   revert t2 i; induction t1 as [|o1 l1 IHl1 r1 IHr1]; intros t2 i; simpl.
   { rewrite Pomap_lookup. by destruct (t2 !! i). }
   unfold compose, flip.
-  destruct t2 as [|l2 o2 r2]; rewrite PNode_lookup.
+  destruct t2 as [|o2 l2 r2]; rewrite PNode_lookup.
   - by destruct i; rewrite ?Pomap_lookup; simpl; rewrite ?Pomap_lookup;
       match goal with |- ?o ≫= _ = _ => destruct o end.
   - destruct i; rewrite ?Pomap_lookup; simpl; auto.
@@ -299,7 +298,7 @@ Proof.
     + by intros [(?&->&?)|].
     + by left; exists i.
   - intros ?? ? [??] ?. by apply Pomap_lookup.
-  - intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
+  - intros ??? ? [??] [??] ?. by apply Pmerge_lookup.
 Qed.
 
 Global Program Instance Pmap_countable `{Countable A} : Countable (Pmap A) := {
diff --git a/theories/zmap.v b/theories/zmap.v
index 32e1ed3c7a93380825cb7b579d87d0975fae488f..a27e69b6b31d47d4f5b22db3f314e6d4d13c1011 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -42,9 +42,9 @@ Global Instance Zomap: OMap Zmap := λ A B f t,
 Global Instance Zmerge: Merge Zmap := λ A B C f t1 t2,
   match t1, t2 with
   | ZMap o1 t1 t1', ZMap o2 t2 t2' =>
-     ZMap (f o1 o2) (merge f t1 t2) (merge f t1' t2')
+     ZMap (diag_None f o1 o2) (merge f t1 t2) (merge f t1' t2')
   end.
-Global Instance Nfmap: FMap Zmap := λ A B f t,
+Global Instance Zfmap: FMap Zmap := λ A B f t,
   match t with ZMap o t t' => ZMap (f <$> o) (f <$> t) (f <$> t') end.
 
 Global Instance: FinMap Z Zmap.
@@ -85,7 +85,7 @@ Proof.
         { left; exists (i, x). by rewrite elem_of_map_to_list. }
         right; exists (i, x). by rewrite elem_of_map_to_list.
   - intros ?? f [??] [|?|?]; simpl; [done| |]; apply (lookup_omap f).
-  - intros ??? f ? [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
+  - intros ??? f [??] [??] [|?|?]; simpl; [done| |]; apply (lookup_merge f).
 Qed.
 
 (** * Finite sets *)