diff --git a/CHANGELOG.md b/CHANGELOG.md
index 22af9f201403fa5442ed4b342c8fdbc8433ad262..77a7838a513a2698f152d4962fcad0529db8149e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -52,15 +52,30 @@ API-breaking change is listed.
   + Maps: Add lemmas `map_disjoint_filter` and `map_filter_union` analogous to
     sets.
 - Add cross split lemma `map_cross_split` for maps
-- Better setoid results for options and maps:
-  + Add instances `map_singleton_equiv_inj` and `map_fmap_equiv_inj`.
+- Setoid results for options:
   + Add instance `option_fmap_equiv_inj`.
-  + Add and generalize `Proper` instances for various operations on maps.
+  + Add `Proper` instances for `union`, `union_with`, `intersection_with`, and
+    `difference_with`.
+  + 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.
+  + Rename `equiv_None` → `None_equiv_eq`.
+  + Replace `equiv_Some_inv_l`, `equiv_Some_inv_r`, `equiv_Some_inv_l'`, and
+    `equiv_Some_inv_r'` by new lemma `Some_equiv_eq` that follows the pattern of
+    other `≡`-inversion lemmas: it uses a `↔` and puts the arguments of `≡` and
+    `=` in consistent order.
+- Setoid results for lists:
+  + Add `≡`-inversion lemmas `nil_equiv_eq`, `cons_equiv_eq`,
+    `list_singleton_equiv_eq`,  and `app_equiv_eq`.
+  + Add lemmas `Permutation_equiv` and `equiv_Permutation`.
+- Setoid results for maps:
+  + Add instances `map_singleton_equiv_inj` and `map_fmap_equiv_inj`.
+  + Add and generalize many `Proper` instances.
   + Add lemma `map_equiv_lookup_r`.
   + Add lemma `map_equiv_iff`.
-- 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.
+  + Rename `map_equiv_empty` → `map_empty_equiv_eq`.
+  + Add `≡`-inversion lemmas `insert_equiv_eq`, `delete_equiv_eq`,
+    `map_union_equiv_eq`, etc.
 - Drop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface.
   + Drop `DiagNone` class.
   + Add `merge_proper` instance.
@@ -102,6 +117,9 @@ s/\brtc_nsteps\b/rtc_nsteps_1/g
 s/\bnsteps_rtc\b/rtc_nsteps_2/g
 s/\brtc_bsteps\b/rtc_bsteps_1/g
 s/\bbsteps_rtc\b/rtc_bsteps_2/g
+# setoid
+s/\bequiv_None\b/None_equiv_eq/g
+s/\bmap_equiv_empty\b/map_empty_equiv_eq/g
 ' $(find theories -name "*.v")
 ```
 
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 7fd11ef73f24a9bea2f2c31bfaa6c0b9b09f9d83..b5a020c2b1cbcebec0a4e689ef4da57f9aa98910 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -2501,12 +2501,7 @@ Section setoid.
 
   Lemma map_equiv_iff (m1 m2 : M A) : m1 ≡ m2 ↔ ∀ i, m1 !! i ≡ m2 !! i.
   Proof. done. Qed.
-  Lemma map_equiv_empty (m : M A) : m ≡ ∅ ↔ m = ∅.
-  Proof.
-    split; [intros Hm; apply map_eq; intros i|intros ->].
-    - generalize (Hm i). by rewrite lookup_empty, equiv_None.
-    - intros ?. rewrite lookup_empty; constructor.
-  Qed.
+
   Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
     m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y.
   Proof. intros Hm Hi. destruct (Hm i); naive_solver. Qed.
@@ -2613,6 +2608,14 @@ Section setoid.
     intros f f' ? m m' ? k; rewrite !lookup_omap. by apply option_bind_proper.
   Qed.
 
+  Global Instance map_filter_proper (P : K * A → Prop) `{!∀ kx, Decision (P kx)} :
+    (∀ k, Proper ((≡) ==> iff) (uncurry P k)) →
+    Proper ((≡@{M A}) ==> (≡)) (filter P).
+  Proof.
+    intros ? m1 m2 Hm i. rewrite !map_filter_lookup.
+    destruct (Hm i); simpl; repeat case_option_guard; try constructor; naive_solver.
+  Qed.
+
   Global Instance map_singleton_equiv_inj :
     Inj2 (=) (≡) (≡) (singletonM (M:=M A)).
   Proof.
@@ -2636,6 +2639,215 @@ Section setoid.
     destruct (m !! i) eqn:?; constructor; eauto.
   Qed.
 End setoid.
+
+(** The lemmas below make it possible to turn an [≡] into an [=]. *)
+Section setoid_inversion.
+  Context `{Equiv A, !Equivalence (≡@{A})}.
+  Implicit Types m : M A.
+
+  Lemma map_empty_equiv_eq m : m ≡ ∅ ↔ m = ∅.
+  Proof.
+    split; [intros Hm; apply map_eq; intros i|intros ->].
+    - generalize (Hm i). by rewrite lookup_empty, None_equiv_eq.
+    - intros ?. rewrite lookup_empty; constructor.
+  Qed.
+
+  Lemma partial_alter_equiv_eq (f : option A → option A) (m1 m2 : M A) i :
+    Proper ((≡) ==> (≡)) f →
+    (∀ x1 mx2, Some x1 ≡ f mx2 → ∃ mx2', Some x1 = f mx2' ∧ mx2' ≡ mx2) →
+    m1 ≡ partial_alter f i m2 ↔ ∃ m2', m1 = partial_alter f i m2' ∧ m2' ≡ m2.
+  Proof.
+    intros ? Hf. split; [|by intros (?&->&<-)]. intros Hm.
+    assert (∃ mx2', m1 !! i = f mx2' ∧ mx2' ≡ m2 !! i) as (mx2'&?&?).
+    { destruct (m1 !! i) as [x1|] eqn:Hix1.
+      - apply (Hf x1 (m2 !! i)). by rewrite <-Hix1, Hm, lookup_partial_alter.
+      - exists (m2 !! i). split; [|done]. apply symmetry, None_equiv_eq.
+        by rewrite <-Hix1, Hm, lookup_partial_alter. }
+    exists (partial_alter (λ _, mx2') i m1). split.
+    - apply map_eq; intros j. destruct (decide (i = j)) as [->|?].
+      + by rewrite !lookup_partial_alter.
+      + by rewrite !lookup_partial_alter_ne.
+    - intros j. destruct (decide (i = j)) as [->|?].
+      + by rewrite lookup_partial_alter.
+      + by rewrite Hm, !lookup_partial_alter_ne.
+  Qed.
+  Lemma alter_equiv_eq (f : A → A) (m1 m2 : M A) i :
+    Proper ((≡) ==> (≡)) f →
+    (∀ x1 x2, x1 ≡ f x2 → ∃ x2', x1 = f x2' ∧ x2' ≡ x2) →
+    m1 ≡ alter f i m2 ↔ ∃ m2', m1 = alter f i m2' ∧ m2' ≡ m2.
+  Proof.
+    intros ? Hf. apply (partial_alter_equiv_eq _ _ _ _ _). intros mx1 [x2|]; simpl.
+    - intros (x2'&->&?)%(inj _)%Hf. exists (Some x2'). by repeat constructor.
+    - intros ->%None_equiv_eq. by exists None.
+  Qed.
+
+  Lemma delete_equiv_eq m1 m2 i :
+    m1 ≡ delete i m2 ↔ ∃ m2', m1 = delete i m2' ∧ m2' ≡ m2.
+  Proof. apply (partial_alter_equiv_eq _ _ _ _ _). intros ?? [=]%None_equiv_eq. Qed.
+  Lemma insert_equiv_eq m1 m2 i x :
+    m1 ≡ <[i:=x]> m2 ↔ ∃ x' m2', m1 = <[i:=x']> m2' ∧ x' ≡ x ∧ m2' ≡ m2.
+  Proof.
+    split; [|by intros (?&?&->&<-&<-)]. intros Hm.
+    assert (is_Some (m1 !! i)) as [x' Hix'].
+    { rewrite Hm, lookup_insert. eauto. }
+    destruct (m2 !! i) as [y|] eqn:?.
+    - exists x', (<[i:=y]> m1). split_and!.
+      + by rewrite insert_insert, insert_id by done.
+      + apply (inj Some). by rewrite <-Hix', Hm, lookup_insert.
+      + by rewrite Hm, insert_insert, insert_id by done.
+    - exists x', (delete i m1). split_and!.
+      + by rewrite insert_delete, insert_id by done.
+      + apply (inj Some). by rewrite <-Hix', Hm, lookup_insert.
+      + by rewrite Hm, delete_insert by done.
+  Qed.
+  Lemma map_singleton_equiv_eq m i x :
+    m ≡ {[i:=x]} ↔ ∃ x', m = {[i:=x']} ∧ x' ≡ x.
+  Proof.
+    rewrite <-!insert_empty, insert_equiv_eq.
+    setoid_rewrite map_empty_equiv_eq. naive_solver.
+  Qed.
+
+  Lemma map_filter_equiv_eq (P : K * A → Prop) `{!∀ kx, Decision (P kx)} (m1 m2 : M A):
+    (∀ k, Proper ((≡) ==> iff) (uncurry P k)) →
+    m1 ≡ filter P m2 ↔ ∃ m2', m1 = filter P m2' ∧ m2' ≡ m2.
+  Proof.
+    intros HP. split; [|by intros (?&->&->)].
+    revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hm.
+    { rewrite map_filter_empty in Hm. exists ∅.
+      by rewrite map_filter_empty, <-map_empty_equiv_eq. }
+    destruct (decide (P (i,x))).
+    - rewrite map_filter_insert in Hm by done.
+      apply insert_equiv_eq in Hm as (x'&m2'&->&?&(m2''&->&?)%IH).
+      exists (<[i:=x']> m2''). split; [|by f_equiv].
+      by rewrite map_filter_insert by (by eapply HP).
+    - rewrite map_filter_insert_not' in Hm by naive_solver.
+      apply IH in Hm as (m2'&->&Hm2). exists (<[i:=x]> m2'). split; [|by f_equiv].
+      assert (m2' !! i = None).
+      { by rewrite <-None_equiv_eq, Hm2, None_equiv_eq. }
+      by rewrite map_filter_insert_not' by naive_solver.
+  Qed.
+End setoid_inversion.
+
+Lemma map_omap_equiv_eq `{Equiv A, !Equivalence (≡@{A}),
+      Equiv B, !Equivalence (≡@{B})}
+    (f : A → option B) (m1 : M B) (m2 : M A) :
+  Proper ((≡) ==> (≡)) f →
+  (∀ y x, Some y ≡ f x → ∃ x', Some y = f x' ∧ x' ≡ x) →
+  m1 ≡ omap f m2 ↔ ∃ m2', m1 = omap f m2' ∧ m2' ≡ m2.
+Proof.
+  intros ? Hf. split; [|by intros (?&->&->)].
+  revert m1. induction m2 as [|i x m2 ? IH] using map_ind; intros m1 Hm.
+  { rewrite omap_empty, map_empty_equiv_eq in Hm. subst m1.
+    exists ∅. by rewrite omap_empty. }
+  rewrite omap_insert in Hm. destruct (f x) as [y|] eqn:Hfx.
+  - apply insert_equiv_eq in Hm as (y'&m1'&->&Hy&(m2'&->&?)%IH).
+    destruct (Hf y' x) as (x'&Hfx'&?).
+    { by rewrite Hfx, Hy. }
+    exists (<[i:=x']> m2'). split; [|by f_equiv].
+    by rewrite omap_insert, <-Hfx'.
+  - apply delete_equiv_eq in Hm as (m1'&->&(m2'&->&?)%IH).
+    exists (<[i:=x]> m2'). split; [|by f_equiv]. by rewrite omap_insert, Hfx.
+Qed.
+Lemma map_fmap_equiv_eq `{Equiv A, !Equivalence (≡@{A}),
+      Equiv B, !Equivalence (≡@{B})} (f : A → B) (m1 : M B) (m2 : M A) :
+  Proper ((≡) ==> (≡)) f →
+  (∀ y x, y ≡ f x → ∃ x', y = f x' ∧ x' ≡ x) →
+  m1 ≡ f <$> m2 ↔ ∃ m2', m1 = f <$> m2' ∧ m2' ≡ m2.
+Proof.
+  intros ? Hf. rewrite map_fmap_alt; setoid_rewrite map_fmap_alt.
+  apply map_omap_equiv_eq; [solve_proper|].
+  intros ?? (?&->&?)%(inj _)%Hf; eauto.
+Qed.
+
+Lemma merge_equiv_eq `{Equiv A, !Equivalence (≡@{A}),
+    Equiv B, !Equivalence (≡@{B}), Equiv C, !Equivalence (≡@{C})}
+    (f : option A → option B → option C) (m1 : M C) (m2a : M A) (m2b : M B) :
+  Proper ((≡) ==> (≡) ==> (≡)) f →
+  (∀ y mx1 mx2,
+    Some y ≡ f mx1 mx2 →
+    ∃ mx1' mx2', Some y = f mx1' mx2' ∧ mx1' ≡ mx1 ∧ mx2' ≡ mx2) →
+  m1 ≡ merge f m2a m2b ↔
+    ∃ m2a' m2b', m1 = merge f m2a' m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
+Proof.
+  intros ? Hf. split; [|by intros (?&?&->&->&->)].
+  revert m1. induction m2a as [|i x m2a ? IH] using map_ind; intros m1.
+  { assert (∀ y x,
+      Some y ≡ f None (Some x) → ∃ x', Some y = f None (Some x') ∧ x' ≡ x).
+    { intros ?? (?&?&?&->%None_equiv_eq&(?&->&?)%Some_equiv_eq)%Hf; eauto. }
+    rewrite merge_empty_l, map_omap_equiv_eq by (done || solve_proper).
+    intros (m2'&->&?). exists ∅, m2'. by rewrite merge_empty_l. }
+  unfold insert at 1, map_insert at 1.
+  rewrite <-(partial_alter_merge_l _ (λ _, f (Some x) (m2b !! i))) by done.
+  destruct (f (Some x) (m2b !! i)) as [y|] eqn:Hfi.
+  - intros (y'&m'&->&Hy&(m2a'&m2b'&->&Hm2a&Hm2b)%IH)%insert_equiv_eq.
+    destruct (Hf y' (Some x) (m2b !! i)) as (mx1&mx2&?&(x'&->&?)%Some_equiv_eq&?).
+    { by rewrite Hy, Hfi. }
+    exists (<[i:=x']> m2a'), (partial_alter (λ _, mx2) i m2b').
+    split_and!; [by apply partial_alter_merge|by f_equiv|].
+    intros j. destruct (decide (i = j)) as [->|?].
+    + by rewrite lookup_partial_alter.
+    + by rewrite Hm2b, lookup_partial_alter_ne.
+  - intros (m'&->&(m2a'&m2b'&->&Hm2a&Hm2b)%IH)%delete_equiv_eq.
+    exists (<[i:=x]> m2a'), m2b'. split_and!; [|by f_equiv|done].
+    apply partial_alter_merge_l, symmetry, None_equiv_eq; simpl.
+    by rewrite Hm2b, Hfi.
+Qed.
+
+Lemma map_union_with_equiv_eq `{Equiv A, !Equivalence (≡@{A})}
+    (f : A → A → option A) (m1 m2a m2b : M A) :
+  Proper ((≡) ==> (≡) ==> (≡)) f →
+  (∀ y x1 x2,
+    Some y ≡ f x1 x2 → ∃ x1' x2', Some y = f x1' x2' ∧ x1' ≡ x1 ∧ x2' ≡ x2) →
+  m1 ≡ union_with f m2a m2b ↔
+    ∃ m2a' m2b', m1 = union_with f m2a' m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
+Proof.
+  intros ? Hf. apply (merge_equiv_eq _ _ _ _ _).
+  intros ? [x1|] [x2|]; simpl;
+    first [intros (?&?&?&?&?)%Hf|intros (?&?&?)%Some_equiv_eq|intros ?%None_equiv_eq];
+    by repeat econstructor.
+Qed.
+Lemma map_intersection_with_equiv_eq `{Equiv A, !Equivalence (≡@{A})}
+    (f : A → A → option A) (m1 m2a m2b : M A) :
+  Proper ((≡) ==> (≡) ==> (≡)) f →
+  (∀ y x1 x2,
+    Some y ≡ f x1 x2 → ∃ x1' x2', Some y = f x1' x2' ∧ x1' ≡ x1 ∧ x2' ≡ x2) →
+  m1 ≡ intersection_with f m2a m2b ↔
+    ∃ m2a' m2b', m1 = intersection_with f m2a' m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
+Proof.
+  intros ? Hf. apply (merge_equiv_eq _ _ _ _ _).
+  intros ? [x1|] [x2|]; simpl;
+    first [intros (?&?&?&?&?)%Hf|intros (?&?&?)%Some_equiv_eq|intros ?%None_equiv_eq];
+    by repeat econstructor.
+Qed.
+Lemma map_difference_with_equiv_eq `{Equiv A, !Equivalence (≡@{A})}
+    (f : A → A → option A) (m1 m2a m2b : M A) :
+  Proper ((≡) ==> (≡) ==> (≡)) f →
+  (∀ y x1 x2,
+    Some y ≡ f x1 x2 → ∃ x1' x2', Some y = f x1' x2' ∧ x1' ≡ x1 ∧ x2' ≡ x2) →
+  m1 ≡ difference_with f m2a m2b ↔
+    ∃ m2a' m2b', m1 = difference_with f m2a' m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
+Proof.
+  intros ? Hf. apply (merge_equiv_eq _ _ _ _ _).
+  intros ? [x1|] [x2|]; simpl;
+    first [intros (?&?&?&?&?)%Hf|intros (?&?&?)%Some_equiv_eq|intros ?%None_equiv_eq];
+    by repeat econstructor.
+Qed.
+
+Lemma map_union_equiv_eq `{Equiv A, !Equivalence (≡@{A})} (m1 m2a m2b : M A) :
+  m1 ≡ m2a ∪ m2b ↔ ∃ m2a' m2b', m1 = m2a' ∪ m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
+Proof.
+  apply map_union_with_equiv_eq; [solve_proper|]. intros ??? ?%(inj _); eauto.
+Qed.
+Lemma map_intersection_equiv_eq `{Equiv A, !Equivalence (≡@{A})} (m1 m2a m2b : M A) :
+  m1 ≡ m2a ∩ m2b ↔ ∃ m2a' m2b', m1 = m2a' ∩ m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
+Proof.
+  apply map_intersection_with_equiv_eq; [solve_proper|]. intros ??? ?%(inj _); eauto.
+Qed.
+Lemma map_difference_equiv_eq `{Equiv A, !Equivalence (≡@{A})} (m1 m2a m2b : M A) :
+  m1 ≡ m2a ∖ m2b ↔ ∃ m2a' m2b', m1 = m2a' ∖ m2b' ∧ m2a' ≡ m2a ∧ m2b' ≡ m2b.
+Proof.
+  apply map_difference_with_equiv_eq; [constructor|]. intros ??? [=]%None_equiv_eq.
+Qed.
 End theorems.
 
 (** ** The seq operation *)
diff --git a/theories/list.v b/theories/list.v
index ef88844b679031164aa2d8bb6b95aea23ae95b43..6087a9ca6b4548017d46e7eadbd5e70a6b83430e 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -3456,6 +3456,40 @@ Section setoid.
   Proof.
     induction n; destruct 2; simpl; repeat (constructor || f_equiv); auto.
   Qed.
+
+  Lemma nil_equiv_eq mx : mx ≡ [] ↔ mx = [].
+  Proof. split; [by inversion_clear 1|intros ->; constructor]. Qed.
+  Lemma cons_equiv_eq l x k : l ≡ x :: k ↔ ∃ x' k', l = x' :: k' ∧ x' ≡ x ∧ k' ≡ k.
+  Proof. split; [inversion 1; naive_solver|naive_solver (by constructor)]. Qed.
+  Lemma list_singleton_equiv_eq l x : l ≡ [x] ↔ ∃ x', l = [x'] ∧ x' ≡ x.
+  Proof. rewrite cons_equiv_eq. setoid_rewrite nil_equiv_eq. naive_solver. Qed.
+  Lemma app_equiv_eq l k1 k2 :
+    l ≡ k1 ++ k2 ↔ ∃ k1' k2', l = k1' ++ k2' ∧ k1' ≡ k1 ∧ k2' ≡ k2.
+  Proof.
+    split; [|intros (?&?&->&?&?); by f_equiv].
+    setoid_rewrite equiv_Forall2. rewrite Forall2_app_inv_r. naive_solver.
+  Qed.
+
+  Lemma equiv_Permutation l1 l2 l3 :
+    l1 ≡ l2 → l2 ≡ₚ l3 → ∃ l2', l1 ≡ₚ l2' ∧ l2' ≡ l3.
+  Proof.
+    intros Hequiv Hperm. revert l1 Hequiv.
+    induction Hperm as [|x l2 l3 _ IH|x y l2|l2 l3 l4 _ IH1 _ IH2]; intros l1.
+    - intros ?. by exists l1.
+    - intros (x'&l2'&->&?&(l2''&?&?)%IH)%cons_equiv_eq.
+      exists (x' :: l2''). by repeat constructor.
+    - intros (y'&?&->&?&(x'&l2'&->&?&?)%cons_equiv_eq)%cons_equiv_eq.
+      exists (x' :: y' :: l2'). by repeat constructor.
+    - intros (l2'&?&(l3'&?&?)%IH2)%IH1. exists l3'. split; [by etrans|done].
+  Qed.
+
+  Lemma Permutation_equiv `{!Equivalence (≡@{A})} l1 l2 l3 :
+    l1 ≡ₚ l2 → l2 ≡ l3 → ∃ l2', l1 ≡ l2' ∧ l2' ≡ₚ l3.
+  Proof.
+    intros Hperm%symmetry Hequiv%symmetry.
+    destruct (equiv_Permutation _ _  _ Hequiv Hperm) as (l2'&?&?).
+    by exists l2'.
+  Qed.
 End setoid.
 
 (** * Properties of the [find] function *)
diff --git a/theories/option.v b/theories/option.v
index 767426f172e95168de65cb553ffbad8b25858d22..a3513f5cb6668f37b73c3cfdcc935e622336b2df 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -129,19 +129,10 @@ Section setoids.
   Global Instance Some_equiv_inj : Inj (≡) (≡@{option A}) Some.
   Proof. by inversion_clear 1. Qed.
 
-  Lemma equiv_None mx : mx ≡ None ↔ mx = None.
+  Lemma None_equiv_eq mx : mx ≡ None ↔ mx = None.
   Proof. split; [by inversion_clear 1|intros ->; constructor]. Qed.
-  Lemma equiv_Some_inv_l mx my x :
-    mx ≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡ y.
-  Proof. destruct 1; naive_solver. Qed.
-  Lemma equiv_Some_inv_r mx my y :
-    mx ≡ my → my = Some y → ∃ x, mx = Some x ∧ x ≡ y.
-  Proof. destruct 1; naive_solver. Qed.
-  Lemma equiv_Some_inv_l' my x : Some x ≡ my → ∃ x', Some x' = my ∧ x ≡ x'.
-  Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed.
-  Lemma equiv_Some_inv_r' `{!Equivalence (≡@{A})} mx y :
-    mx ≡ Some y → ∃ y', mx = Some y' ∧ y ≡ y'.
-  Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed.
+  Lemma Some_equiv_eq mx y : mx ≡ Some y ↔ ∃ y', mx = Some y' ∧ y' ≡ y.
+  Proof. split; [inversion 1; naive_solver|naive_solver (by constructor)]. Qed.
 
   Global Instance is_Some_proper : Proper ((≡@{option A}) ==> iff) is_Some.
   Proof. inversion_clear 1; split; eauto. Qed.
@@ -199,8 +190,8 @@ Proof.
   destruct mx; simpl; split.
   - intros ?%(inj Some). eauto.
   - intros (? & ->%(inj Some) & ?). constructor. done.
-  - intros ?%symmetry%equiv_None. done.
-  - intros (? & ? & ?). done.
+  - intros [=]%symmetry%None_equiv_eq.
+  - intros (? & [=] & ?).
 Qed.
 Lemma fmap_Some_equiv_1 {A B} `{Equiv B} `{!Equivalence (≡@{B})} (f : A → B) mx y :
   f <$> mx ≡ Some y → ∃ x, mx = Some x ∧ y ≡ f x.
@@ -321,6 +312,19 @@ Section union_intersection_difference.
   Proof. by intros ? [?|] [?|]; compute; rewrite 1?(comm f). Qed.
   Global Instance difference_with_right_id : RightId (=) None (difference_with f).
   Proof. by intros [?|]. Qed.
+
+  Global Instance union_with_proper `{Equiv A} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{option A}) ==> (≡) ==> (≡)) union_with.
+  Proof. intros ?? Hf; do 2 destruct 1; try constructor; by try apply Hf. Qed.
+  Global Instance intersection_with_proper `{Equiv A} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{option A}) ==> (≡) ==> (≡)) intersection_with.
+  Proof. intros ?? Hf; do 2 destruct 1; try constructor; by try apply Hf. Qed.
+  Global Instance difference_with_proper `{Equiv A} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{option A}) ==> (≡) ==> (≡)) difference_with.
+  Proof. intros ?? Hf; do 2 destruct 1; try constructor; by try apply Hf. Qed.
+  Global Instance union_proper `{Equiv A} :
+    Proper ((≡@{option A}) ==> (≡) ==> (≡)) union.
+  Proof. apply union_with_proper. by constructor. Qed.
 End union_intersection_difference.
 
 (** * Tactics *)